coq - The formal proof system

Age	Commit message (Expand)	Author
2006-10-28	Extension du polymorphisme de sorte au cas des définitions dans Type.	herbelin
2006-05-23	Nouvelle implantation du polymorphisme de sorte pour les familles inductives	herbelin
2006-03-17	Modification des propriétés (svn:executable)	notin
2006-01-28	Ajout option 'using lemmas' à auto/trivial/eauto	herbelin
2006-01-28	Suppression code pour hints nommés à la V7 (voire à la V6...)	herbelin
2006-01-24	Suppression de la dépendance en Map.fold de ocaml dont la sémantique a	herbelin
2006-01-11	removes several warnings in contrib/interface	bertot
2005-12-26	Renommage des Ppnew en Pp (et déplacement dans parsing); renommage des G_*...	herbelin
2005-12-26	Achèvement suppression traducteur dans contrib/interface	herbelin
2005-12-02	Changement des named_context	gregoire
2004-12-07	* added subst_evaluable_reference	sacerdot
2004-09-17	restructuration des printers: proofs passe avant parsing	barras
2004-09-03	premiere reorganisation de l\'unification	barras
2004-07-16	Nouvelle en-tête	herbelin
2003-11-13	factorisation et generalisation des clauses	barras
2003-04-07	Globalisation des noms de tactiques dans les définitions de tactiques	herbelin
2002-12-19	simplification de solve_subgoal: n'utilise plus frontier	barras
2002-12-09	Ajout Simpl et Change sur des sous-termes	herbelin
2002-11-14	Réforme de l'interprétation des termes :	herbelin
2002-05-29	Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...	herbelin
2002-02-15	petits changements cosmetiques sur les tactiques	barras
2001-12-18	There remained traces of streams with the old syntax.	bertot
2001-12-18	Integrating the Ltac language and the Blast tool into the interface	bertot