coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Finish fix for the treatment of [inverse] in [setoid_rewrite], making a	msozeau	2008-12-16
*	Fix looping class resolution bug discovered by B. Aydemir and use the	msozeau	2008-12-14
*	Add the ability to declare [Hint Extern]'s with no pattern.	msozeau	2008-09-07
*	Uniformisation du format des messages d'erreur (commencent par une	herbelin	2008-07-17
*	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
*	Move exception-handling code for catching tactics failure	msozeau	2008-05-01
*	Fix eauto still using delta when it shouldn't (should make CoRN compile	msozeau	2008-04-29
*	Backtrack on using metas eagerly in auto, only done in "new auto" for	msozeau	2008-04-28
*	- Fix bug in unification not taking into account the right meta	msozeau	2008-04-27
*	- Add pretty-printers for Idpred, Cpred and transparent_state, used for	msozeau	2008-04-24
*	- Parameterize unification by two sets of transparent_state, one for open	msozeau	2008-04-21
*	Bugs, nettoyage, et améliorations diverses	herbelin	2008-04-13
*	Erreur ou acceptation silencieuce plutôt qu'avertissement systématique quand	herbelin	2008-04-04
*	correction d'un bug d'efficacite dans Function (+ ajout de eauto_with_bases)	jforest	2008-03-08
*	Backtrack changes on eauto, move specialized version of eauto in	msozeau	2008-02-14
*	Debugging of the class_setoid tactic and eauto. Prepare for move from	msozeau	2008-02-13
*	Fix the clrewrite tactic, change Relations.v to work on relations in Prop	msozeau	2008-02-09
*	Change implementation of resolution for typeclasses to use a customized	msozeau	2008-02-08
*	Work-in-progress to make eauto accept a list of goals as input and	msozeau	2008-02-06
*	Factorisation des opérations sur le type option de Util dans un module	aspiwack	2007-12-05
*	Slight cleanup of refl_omega.ml : in particular it uses now list	letouzey	2007-07-11
*	Nouvelle stratégie d'unification des types des with-bindings dans	herbelin	2007-05-22
*	Ajout de la possibilité d'utiliser les evars dans apply_in et elim_in.	herbelin	2007-04-28
*	Suite unification apply et eapply (l'un et l'autre profite maintenant	herbelin	2007-04-16
*	Essai de partage de code entre apply et eapply	herbelin	2007-04-15
*	Correction d'une tentative incorrecte (révision 9266) de clarification	herbelin	2006-10-25
*	Généralisation de with_occurrence (ex occurrence) et de red_expr pour perme...	herbelin	2006-05-30
*	Standardisation nom option_app en option_map	herbelin	2006-04-27
*	Debugging en syntaxe v8	herbelin	2006-02-05
*	Ajout option 'using lemmas' à auto/trivial/eauto	herbelin	2006-01-28
*	Suppression de la dépendance en Map.fold de ocaml dont la sémantique a	herbelin	2006-01-24
*	Export eassumption	herbelin	2006-01-19
*	Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...	herbelin	2005-12-26
*	Ajout printer pr_lconstr aux extensions de syntaxe pour les arguments de tact...	herbelin	2005-12-21
*	Changement des named_context	gregoire	2005-12-02
*	Nettoyage suite à la détection par défaut des variables inutilisées par o...	herbelin	2005-11-08
*	* added subst_evaluable_reference	sacerdot	2004-12-07
*	unification encore...	barras	2004-09-08
*	deuxieme vague de modifs: evar_defs fonctionnel	barras	2004-09-07
*	premiere reorganisation de l\'unification	barras	2004-09-03
*	Nouvelle en-tête	herbelin	2004-07-16
*	Nouvelle tactique EExists	clrenard	2003-12-01
*	New tactics : econstructor, eleft, eright, esplit	clrenard	2003-11-17
*	Nettoyage	herbelin	2003-11-08
*	Nouvelle mouture du traducteur v7->v8	herbelin	2003-08-11
*	Globalisation des noms de tactiques dans les définitions de tactiques	herbelin	2003-04-07
*	* empty log message *	barras	2003-03-12
*	Restructuration interpréteur de tactique: plus d'évaluation partielle à la...	herbelin	2003-01-19
*	Option pour rendre les vérifications du refiner optionnelle	herbelin	2002-12-09