coq - The formal proof system

Age	Commit message (Expand)	Author
2006-04-28	Standardisation du nom des méthodes de Evd	herbelin
2006-04-28	Suppression des fichiers .cvsignore, rendus obsolètes par le systèmes des '...	notin
2006-04-27	Standardisation nom option_app en option_map	herbelin
2006-04-26	Diverses corrections de l'afficheur et du traducteur pour s'assurer de	herbelin
2006-04-12	induction on multiple arguments made better:	courtieu
2006-04-11	adding a new tactic [intro_avoiding idl] which acts as intro but prevents the	jforest
2006-04-06	Enlevement de message d'erreur garbage.	courtieu
2006-04-05	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-02	Correction bug 1119 (inversion marche a moitie dans Type)	herbelin
2006-03-22	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-21	+ destruct now works as induction on multiple arguments :	jforest
2006-03-12	-Debugging multiple induction, a bug appeared when having function	courtieu
2006-03-05	Correction bug 984 via introduction TacCall(loc,r,[]) pour signifier une réf...	herbelin
2006-03-02	Correction bug #1097 (dû à une typo...)	herbelin
2006-02-23	trying to fix a bug in pazrameter order in the multiple induction	coq
2006-02-17	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-16	added isProd to term.mli.	coq
2006-02-15	continuing the generalization of "induction". Now induction schemes	coq
2006-02-10	induction now admits multiple induction arguments. The principle must	coq
2006-02-05	Debugging en syntaxe v8	herbelin
2006-01-28	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-24	Suppression de la dépendance en Map.fold de ocaml dont la sémantique a	herbelin
2006-01-21	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-20	Ajout de la contrainte de résoudre l'assertion dans 'assert by'	herbelin
2006-01-19	Conséquences supplémentaires de la fin du support v7	herbelin
2006-01-19	Export eassumption	herbelin
2006-01-16	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-11	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
2005-12-30	Nettoyage coqlib	herbelin
2005-12-26	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-21	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-02	Changement des named_context	gregoire
2005-11-17	A la demande de Julien Forest	letouzey