coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Petit bug Declare Implicit Tactic	herbelin	2005-09-10
*	Nouvelle déclaration 'Declare Implicit Tactic' pour automatiser la résoluti...	herbelin	2005-09-09
*	Réparation bug #1000 (attendre fin de toutes les intros avant d'effacer les ...	herbelin	2005-09-08
*	Réparation bug #1004; nettoyage	herbelin	2005-09-08
*	Sur le conseil de X.Leroy: x=[\|\|] devient Array.length x=0	letouzey	2005-08-19
*	Correction double bug #986: Fold ne préserve pas nécessairement le typage e...	herbelin	2005-07-13
*	essai de typage des instantiations d\'evars	barras	2005-06-06
*	New commit to allow definitions of morphisms on relations whose carrier is	sacerdot	2005-05-24
*	New command: "Print Ltac qualid" to print user defined tactics.	sacerdot	2005-05-20
*	Adoption du nom canonique global_of_constr pour éviter confusion avec type r...	herbelin	2005-05-20
*	Déplacement et export de locate_global (ex-locate_reference) de tacinterp ve...	herbelin	2005-05-20
*	Setoid_replace: improved error message when trying to replace a term in a	sacerdot	2005-05-19
*	A wish by Bas Spitters granted: a little more of unification up to	sacerdot	2005-05-19
*	Implemented autorewrite with ... in hyp [using ...].	sacerdot	2005-05-18
*	Extension de Tactic Notation pour permettre d'tendre et de faire rffrence aux...	herbelin	2005-05-17
*	Globalisation des Tactic Notation	herbelin	2005-05-15
*	Allow auto to have a parametric argument (wish #967)	herbelin	2005-05-15
*	Improved order of interpretation of atomic tactics (cf bug #952)	herbelin	2005-04-29
*	Ajout de l'axiome du but prouve par la tactique simplifi	coq	2005-03-22
*	Correction bug de dependent_hyps qui ne met pas à jour le type des hyps dép...	herbelin	2005-03-20
*	Le type d'un Let est considéré comme 'user-provided' par le noyau et doit d...	herbelin	2005-03-19
*	Report depuis la V8.0pl2 de la correction d'un bug du traducteur	herbelin	2005-03-19
*	appel de Simplify depuis Coq	coq	2005-03-18
*	Fix bug #931: leave dependent evars as such for refine	herbelin	2005-03-08
*	Added 'clear - id' to clear all hypotheses except the ones dependent in the s...	herbelin	2005-03-07
*	Moving subst_inductive from tacinterp to inductiveops for better for reuse in...	herbelin	2005-02-18
*	Standardisation of function names about global references (especially, renami...	herbelin	2005-02-18
*	Moving subst_inductive from tacinterp to inductiveops for better for reuse in...	herbelin	2005-02-18
*	Ajout constructeur External pour appel outil externe à Coq	herbelin	2005-02-04
*	Compatibilité ocamlweb pour cible doc	herbelin	2005-01-21
*	Compatibilité ocamlweb pour cible doc	herbelin	2005-01-21
*	Bug (reported by Lionel Mamane) fixed: the test for non-occurrence of the	sacerdot	2005-01-18
*	Bug fixed (reported by Roland): the setoire_rewrite in tactic did not work	sacerdot	2005-01-17
*	HUGE COMMIT	sacerdot	2005-01-03
*	Partie reduction_of_red_expr de tacred.ml qui dépend de la vm maintenant dan...	herbelin	2005-01-02
*	ExtraRedExpr maintenant sans argument: pas très souple mais au moins convien...	herbelin	2004-12-29
*	Restauration type casted_open_constr pour tactique refine car l'unification n...	herbelin	2004-12-09
*	* added subst_evaluable_reference	sacerdot	2004-12-07
*	The type Pattern.constr_label was isomorphic to Libnames.global_reference.	sacerdot	2004-12-07
*	Uniformisation du nom d'entrée openconstr en le nom du type open_constr	herbelin	2004-12-06
*	Garder les cast semble décidément le meilleur moyen de rester synchrone ave...	herbelin	2004-12-06
*	Suppression des cast après avoir utiliser l'information de type (Tacinv envo...	herbelin	2004-12-06
*	Déplacement de la coercion vis à vis du but au niveau de Refine	herbelin	2004-12-06
*	Déplacement de la coercion vis à vis du but au niveau de Refine suite à ch...	herbelin	2004-12-06
*	Réparation bug #888 (les tactiques fix et cofix exigent autant de sous-buts ...	herbelin	2004-12-06
*	Généralisation de CastedOpenConstrArg en OpenConstrArg, à charge des tacti...	herbelin	2004-12-06
*	MAJ affichage nouvelle syntaxe	herbelin	2004-12-06
*	Bug 'set n in * \|-'	herbelin	2004-12-04
*	backtrack of the last commit (it was my fault: the code is used by	sacerdot	2004-11-26
*	unused function in the interface	sacerdot	2004-11-26