coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	cleaning	coq	2006-02-17
*	bug correction in the decomposition of an induction scheme.	coq	2006-02-17
*	changed the decomposition of an induction scheme	coq	2006-02-17
*	added isProd to term.mli.	coq	2006-02-16
*	continuing the generalization of "induction". Now induction schemes	coq	2006-02-15
*	induction now admits multiple induction arguments. The principle must	coq	2006-02-10
*	Debugging en syntaxe v8	herbelin	2006-02-05
*	Réorganisation de la structure interne des types de déclarations (decl_kinds)	herbelin	2006-01-28
*	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
*	Messages de idtac et fail peuvent maintenant être des listes de string, int ...	herbelin	2006-01-21
*	Ajout niveau utilisateur de la tacticielle 'complete'; messages de idtac et f...	herbelin	2006-01-21
*	Backtrack commit précédent (incompatible avec le choix de prendre Idtac com...	herbelin	2006-01-21
*	Ajout de la contrainte de résoudre l'assertion dans 'assert by'	herbelin	2006-01-20
*	Conséquences supplémentaires de la fin du support v7	herbelin	2006-01-19
*	Export eassumption	herbelin	2006-01-19
*	Ajout motif d'introduction "?" (IntroAnonymous) pour laisser Coq	herbelin	2006-01-16
*	Code redondant	herbelin	2006-01-16
*	- Tactic "assert" now accepts "as" intro patterns and "by" tactic clauses	herbelin	2006-01-16
*	Standardisation du nom de subst_raw en subst_rawconstr	herbelin	2006-01-11
*	Standardisation du nom de subst_raw en subst_rawconstr	herbelin	2006-01-11
*	Résidus du traducteur v7 -> v8	herbelin	2006-01-11
*	Restructuration et simplification des fonctions d'affichage, de détypage	herbelin	2006-01-11
*	Ajout paramétricité du nom de la base de hint dans auto et trivial	herbelin	2006-01-11
*	Nettoyage coqlib	herbelin	2005-12-30
*	Renommage des Ppnew en Pp (et déplacement dans parsing); renommage des G_*...	herbelin	2005-12-26
*	Petite correction nom QuantHypArgType suite suppression traducteur	herbelin	2005-12-26
*	Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...	herbelin	2005-12-26
*	Prise en compte de l'information que certaines tactiques attendent un type (u...	herbelin	2005-12-21
*	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
*	A la demande de Julien Forest	letouzey	2005-11-17
*	Nettoyage suite à la détection par défaut des variables inutilisées par o...	herbelin	2005-11-08
*	Confusion message erreur détectée par nouveau warning X de ocaml 3.09	herbelin	2005-11-04
*	Types inductifs parametriques	mohring	2005-11-02
*	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