coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	induction on multiple arguments made better:	courtieu	2006-04-12
*	adding a new tactic [intro_avoiding idl] which acts as intro but prevents the	jforest	2006-04-11
*	Enlevement de message d'erreur garbage.	courtieu	2006-04-06
*	resolution du bug/souhait #1101 : rewrite setoid dans les hypotheses	letouzey	2006-04-05
*	ajout d'un rattrapage d'erreur pour "induction using".	courtieu	2006-04-05
*	Correction bug 1119 (inversion marche a moitie dans Type)	herbelin	2006-04-02
*	Made pretyping a functor over a coercion implementation. Pretyping.Default us...	msozeau	2006-03-22
*	- Réintroduction d'un parseur de pattern (q_constr.ml4) à usage de	herbelin	2006-03-22
*	+ destruct now works as induction on multiple arguments :	jforest	2006-03-21
*	-Debugging multiple induction, a bug appeared when having function	courtieu	2006-03-12
*	Correction bug 984 via introduction TacCall(loc,r,[]) pour signifier une réf...	herbelin	2006-03-05
*	Correction bug #1097 (dû à une typo...)	herbelin	2006-03-02
*	trying to fix a bug in pazrameter order in the multiple induction	coq	2006-02-23
*	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