coq - The formal proof system

Age	Commit message (Expand)	Author
2010-07-22	Extension of the recursive notations mechanism	herbelin
2010-07-22	Simplified the way internalization_data (i.e. bindings of bound vars	herbelin
2010-07-22	Constrintern: unified push_name_env and push_loc_name_env; made	herbelin
2010-07-22	Switch to American spelling for "internalise" and "internalisation"	herbelin
2010-06-22	New script dev/tools/change-header to automatically update Coq files headers.	herbelin
2010-04-29	Various minor improvements of comments in mli for ocamldoc	letouzey
2010-04-29	Remove the svn-specific $Id$ annotations	letouzey
2010-04-29	Move from ocamlweb to ocamdoc to generate mli documentation	pboutill
2010-01-28	Backport fixes in Instance declarations to Program Instance.	msozeau
2009-11-11	Promote evar_defs to evar_map (in Evd)	glondu
2009-11-11	Improving abbreviations/notations + backtrack of semantic change in r12439	herbelin
2009-11-08	Restructuration of command.ml + generic infrastructure for inductive schemes	herbelin
2009-09-17	Delete trailing whitespaces in all .{v,ml} files	glondu
2009-06-18	Use more consistent resolution parameters in Program and regular typing	msozeau
2009-03-28	Rewrite of Program Fixpoint to overcome the previous limitations:	msozeau
2009-01-17	DISCLAIMER	puech
2008-12-29	- Added support for subterm matching in SearchAbout.	herbelin
2008-11-09	More factorization of inductive/record and typeclasses: move class	msozeau
2008-10-22	Affichage des notations récursives:	herbelin
2008-09-11	Add enough information to correctly globalize recursive calls in inductive and	msozeau
2008-06-25	Création du fichier dumpglob.ml, qui rassemble les fonctions de globalisatio...	notin
2008-05-30	Improvements on coqdoc by adding more information into .glob	msozeau
2008-05-06	Postpone the search for the recursive argument index from the user given	msozeau
2008-03-24	Finish fix in command where we still lost information on what was a type	msozeau
2008-03-15	Do a second pass on the treatment of user-given implicit arguments. Now	msozeau
2007-12-31	Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,...	msozeau
2007-07-02	Fix bug in subst_cases_pattern when aliasing recursive notations.	msozeau
2007-05-06	Nouveaux changements autour des implicites (notamment suite à	herbelin
2007-04-29	Multiples changements autour des implicites :	herbelin
2007-03-28	Support for implicit formal argument types in Program ; parse types in type s...	msozeau
2007-02-13	Réactivation du filtrage d'ordre 2 dans ltac qui avait cessé de	herbelin
2006-09-20	Declarative Proof Language: main commit	corbinea
2006-09-01	Export de fonctions d'interprétation acceptant des evars non résolues	herbelin
2005-12-26	Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...	herbelin
2005-12-21	Restructuration des points d'entrée de Pretyping et Constrintern	herbelin
2005-09-09	Conséquences nettoyage pretyping.ml	herbelin
2005-01-21	Compatibilité ocamlweb pour cible doc	herbelin
2004-07-16	Nouvelle en-tête	herbelin
2004-04-17	pb facto des Fixpoint + erreur avec -dump-glob et Load	barras
2004-03-27	Gestion maintenant purement fonctionnelle des implicites des point-fixes; ajo...	herbelin
2003-11-24	Prise en compte des defs syntaxiques dans is_global et global_reference qui p...	herbelin
2003-10-14	Plus d'uniformite dans la gestion des implicites d'inductifs; nouvelles entre...	herbelin
2003-10-08	Prise en compte des paramètres implicites d'inductifs pour la globalisation ...	herbelin
2003-09-06	cosmetique	herbelin
2003-05-21	Suppression définitive de lmatch et or_metanum dans tacinterp	herbelin
2003-05-19	Renommage CMeta en CPatVar qui sert à saisir les PMeta de Pattern	herbelin
2003-04-09	Mécanisme plus simple et efficace pour traduire les implicites	herbelin
2003-04-07	Globalisation des noms de tactiques dans les définitions de tactiques	herbelin
2003-03-29	Implicit Variables Type dans les inductive	herbelin
2003-01-19	Restructuration interpréteur de tactique: plus d'évaluation partielle à la...	herbelin