coq - The formal proof system

Age	Commit message (Expand)	Author
2009-03-20	Directory 'contrib' renamed into 'plugins', to end confusion with archive of ...	letouzey
2009-03-16	Cleaning/improving the use of the "in" clause (e.g. "unfold foo in H at 4"	herbelin
2009-03-14	Cleaning/uniformizing the interface of tacticals.mli	herbelin
2008-12-28	- Another bug in get_sort_family_of (sort-polymorphism of constants and	herbelin
2008-12-26	11715 continued	herbelin
2008-09-07	Add the ability to declare [Hint Extern]'s with no pattern.	msozeau
2008-09-07	Fixes in typeclasses resolution. Avoid reducing instances types before	msozeau
2008-06-27	Enhanced discrimination nets implementation, which can now work with	msozeau
2008-06-10	- Officialisation de la notation "pattern c at -1" (cf wish 1798 sur coq-bugs)	herbelin
2008-04-28	Backtrack on using metas eagerly in auto, only done in "new auto" for	msozeau
2008-04-21	- Parameterize unification by two sets of transparent_state, one for open	msozeau
2008-04-04	Correction problème de compil (blast.ml)	herbelin
2008-03-06	Syntax changes in typeclasses, remove "?" for usual implicit arguments	msozeau
2007-12-05	Factorisation des opérations sur le type option de Util dans un module	aspiwack
2007-08-27	Oubli dans la révision 10098 (nettoyage body_of_type)	herbelin
2007-07-11	Slight cleanup of refl_omega.ml : in particular it uses now list	letouzey
2007-04-28	Ajout de la possibilité d'utiliser les evars dans apply_in et elim_in.	herbelin
2007-04-16	Export de simplest_eapply, utilisé dans la contrib interface	notin
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