coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Correcting error message when adding Setoid, Relation or morphism (bug #1626)	jforest	2007-10-02
*	Découpage de Setoid.v	notin	2007-09-27
*	Correction du bug #1634 + ajout de bugs dans la test-suite	notin	2007-08-22
*	Correction du bug #1322	notin	2007-08-16
*	A fix for bug #1397:	letouzey	2007-05-23
*	Nouvelle stratégie d'unification des types des with-bindings dans	herbelin	2007-05-22
*	- Propagation des evars non résolues vers les with_bindings; permet par exemple	herbelin	2007-05-20
*	Correction des bugs #1537 (anomalie sur signature incomplète) et #1536	herbelin	2007-05-17
*	Multiples changements autour des implicites :	herbelin	2007-04-29
*	New keyword "Inline" for Parameters and Axioms for automatic	soubiran	2007-04-25
*	Nettoyage des tactiques basées sur "simpl" (delta-réduction cachant	herbelin	2007-04-13
*	Une passe sur les warnings (ajout Options.warn déclenchée par compile-verbo...	herbelin	2007-02-24
*	Ajout fonction clenv_conv_leq pour résoudre les pbs de la forme	herbelin	2007-02-22
*	Raffinement de l'unification de "apply": mémorisation de certains	herbelin	2006-11-19
*	Quick hack to solve to complexity issue in function mark_occur	herbelin	2006-11-01
*	Retour sur la modification apportée en r9289, et nouvelle correction du bug ...	notin	2006-10-31
*	Affichage d'un message d'erreur losque qu'une relation n'a pas été déclar�...	notin	2006-10-26
*	Correction du bug #1255 (réécriture setoid sous un produit)	notin	2006-10-20
*	mise a jour du nouveau ring et ajout du nouveau field, avant renommages	barras	2006-09-26
*	+ Changing "in <hyp>" to "in <clause>" (no at, no InValue and no	jforest	2006-08-22
*	reparation pour le bug #1072 (soufflee par J. Forest):	letouzey	2006-06-06
*	encore un correctif sur le rewrite H in setoid:	letouzey	2006-05-05
*	Standardisation nom option_app en option_map	herbelin	2006-04-27
*	resolution du bug/souhait #1101 : rewrite setoid dans les hypotheses	letouzey	2006-04-05
*	Réorganisation de la structure interne des types de déclarations (decl_kinds)	herbelin	2006-01-28
*	Restructuration et simplification des fonctions d'affichage, de détypage	herbelin	2006-01-11
*	Renommage des Ppnew en Pp (et déplacement dans parsing); renommage des G_*...	herbelin	2005-12-26
*	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
*	Sur le conseil de X.Leroy: x=[\|\|] devient Array.length x=0	letouzey	2005-08-19
*	New commit to allow definitions of morphisms on relations whose carrier is	sacerdot	2005-05-24
*	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
*	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
*	Names.substitution (and related functions) and Term.subst_mps moved to	sacerdot	2004-11-16
*	Changement dans les boxed values .	gregoire	2004-11-12
*	Factorisation cut_replacing	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