coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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-09-07
*	Enhanced discrimination nets implementation, which can now work with	msozeau	2008-06-27
*	- Officialisation de la notation "pattern c at -1" (cf wish 1798 sur coq-bugs)	herbelin	2008-06-10
*	Backtrack on using metas eagerly in auto, only done in "new auto" for	msozeau	2008-04-28
*	- Parameterize unification by two sets of transparent_state, one for open	msozeau	2008-04-21
*	Correction problème de compil (blast.ml)	herbelin	2008-04-04
*	Syntax changes in typeclasses, remove "?" for usual implicit arguments	msozeau	2008-03-06
*	Factorisation des opérations sur le type option de Util dans un module	aspiwack	2007-12-05
*	Oubli dans la révision 10098 (nettoyage body_of_type)	herbelin	2007-08-27
*	Slight cleanup of refl_omega.ml : in particular it uses now list	letouzey	2007-07-11
*	Ajout de la possibilité d'utiliser les evars dans apply_in et elim_in.	herbelin	2007-04-28
*	Export de simplest_eapply, utilisé dans la contrib interface	notin	2007-04-16
*	Extension du polymorphisme de sorte au cas des définitions dans Type.	herbelin	2006-10-28
*	Nouvelle implantation du polymorphisme de sorte pour les familles inductives	herbelin	2006-05-23
*	Modification des propriétés (svn:executable)	notin	2006-03-17
*	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-28
*	Suppression de la dépendance en Map.fold de ocaml dont la sémantique a	herbelin	2006-01-24
*	removes several warnings in contrib/interface	bertot	2006-01-11
*	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-26
*	Changement des named_context	gregoire	2005-12-02
*	* added subst_evaluable_reference	sacerdot	2004-12-07
*	restructuration des printers: proofs passe avant parsing	barras	2004-09-17
*	premiere reorganisation de l\'unification	barras	2004-09-03
*	Nouvelle en-tête	herbelin	2004-07-16
*	factorisation et generalisation des clauses	barras	2003-11-13
*	Globalisation des noms de tactiques dans les définitions de tactiques	herbelin	2003-04-07
*	simplification de solve_subgoal: n'utilise plus frontier	barras	2002-12-19
*	Ajout Simpl et Change sur des sous-termes	herbelin	2002-12-09
*	Réforme de l'interprétation des termes :	herbelin	2002-11-14
*	Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...	herbelin	2002-05-29
*	petits changements cosmetiques sur les tactiques	barras	2002-02-15
*	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	2001-12-18