coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	Réparation incompatibilité de comportement introduite lors de mise en compa...	herbelin	2004-11-22
*	Expansion Case dans injection et discriminate (cf bug #829)	herbelin	2004-11-21
*	New command "Print Rewrite HindDb dbname".	sacerdot	2004-11-17
*	Names.substitution (and related functions) and Term.subst_mps moved to	sacerdot	2004-11-16
*	IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).	sacerdot	2004-11-16
*	Mise en conformité de Derive Inversion et Derive Dependent Inversion avec la...	herbelin	2004-11-15
*	Changement dans les boxed values .	gregoire	2004-11-12
*	Added code to get rid of duplicate rewriting rules.	sacerdot	2004-10-28
*	Ajout 'dependent rewrite in'	herbelin	2004-10-28
*	Factorisation cut_replacing	herbelin	2004-10-27
*	Restructuration fonctions de réécriture depuis égalité dépendante	herbelin	2004-10-27
*	Restructuration fonctions de réécriture depuis égalité dépendante; facto...	herbelin	2004-10-27
*	Word "setoid" banned from the error messages. "relation" used instead.	sacerdot	2004-10-25
*	Missing check implemented (closes a bug from Bas Spitters).	sacerdot	2004-10-25
*	The morphism lemma type was simplified only in modules and not in module	sacerdot	2004-10-21
*	Error message improved.	sacerdot	2004-10-21
*	COMMITED BYTECODE COMPILER	barras	2004-10-20
*	The bug already closed in revision 1.90 was reintroduced again.	sacerdot	2004-10-20
*	Proof term size reduction (again).	sacerdot	2004-10-19
*	* Code simplification and clean-up. In particular there is no more code	sacerdot	2004-10-18
*	Code simplification and clean-up.	sacerdot	2004-10-18
*	The lem field was not computed properly for morphisms whose argument was	sacerdot	2004-10-18
*	The "lem" field of a morphism used to be the compatibility proof, but it	sacerdot	2004-10-18
*	Bug fixed: relations quantified more than once where abstracted in the wrong	sacerdot	2004-10-18
*	More informative error message when the tactic tries to generate a new	sacerdot	2004-10-18
*	zeta flag added to reduce LetIns in a morphism type. Morphisms with local	sacerdot	2004-10-18
*	Wrong comment committed. The tactic behaves correctly only when the	sacerdot	2004-10-15
*	Wish of Maggesi implemented: the type of the morphism compatibility lemma	sacerdot	2004-10-15