coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	Improvements on coqdoc by adding more information into .glob	msozeau	2008-05-30
*	Postpone the search for the recursive argument index from the user given	msozeau	2008-05-06
*	Finish fix in command where we still lost information on what was a type	msozeau	2008-03-24
*	Do a second pass on the treatment of user-given implicit arguments. Now	msozeau	2008-03-15
*	Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,...	msozeau	2007-12-31
*	Fix bug in subst_cases_pattern when aliasing recursive notations.	msozeau	2007-07-02
*	Nouveaux changements autour des implicites (notamment suite à	herbelin	2007-05-06
*	Multiples changements autour des implicites :	herbelin	2007-04-29
*	Support for implicit formal argument types in Program ; parse types in type s...	msozeau	2007-03-28
*	Réactivation du filtrage d'ordre 2 dans ltac qui avait cessé de	herbelin	2007-02-13
*	Declarative Proof Language: main commit	corbinea	2006-09-20
*	Export de fonctions d'interprétation acceptant des evars non résolues	herbelin	2006-09-01
*	Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...	herbelin	2005-12-26
*	Restructuration des points d'entrée de Pretyping et Constrintern	herbelin	2005-12-21
*	Conséquences nettoyage pretyping.ml	herbelin	2005-09-09
*	Compatibilité ocamlweb pour cible doc	herbelin	2005-01-21
*	Nouvelle en-tête	herbelin	2004-07-16
*	pb facto des Fixpoint + erreur avec -dump-glob et Load	barras	2004-04-17
*	Gestion maintenant purement fonctionnelle des implicites des point-fixes; ajo...	herbelin	2004-03-27
*	Prise en compte des defs syntaxiques dans is_global et global_reference qui p...	herbelin	2003-11-24
*	Plus d'uniformite dans la gestion des implicites d'inductifs; nouvelles entre...	herbelin	2003-10-14
*	Prise en compte des paramètres implicites d'inductifs pour la globalisation ...	herbelin	2003-10-08
*	cosmetique	herbelin	2003-09-06
*	Suppression définitive de lmatch et or_metanum dans tacinterp	herbelin	2003-05-21
*	Renommage CMeta en CPatVar qui sert à saisir les PMeta de Pattern	herbelin	2003-05-19
*	Mécanisme plus simple et efficace pour traduire les implicites	herbelin	2003-04-09
*	Globalisation des noms de tactiques dans les définitions de tactiques	herbelin	2003-04-07
*	Implicit Variables Type dans les inductive	herbelin	2003-03-29
*	Restructuration interpréteur de tactique: plus d'évaluation partielle à la...	herbelin	2003-01-19
*	Prise en compte des scopes traversés dans les notations	herbelin	2002-12-15
*	Re-déplacement du résultat de Grammar au niveau constr_expr	herbelin	2002-12-02
*	Réforme de l'interprétation des termes :	herbelin	2002-11-14