coq - The formal proof system

Age	Commit message (Expand)	Author
2007-10-05	Added the automatic generation of the boolean equality if possible and the	vsiles
2007-10-03	Ajout de eelim, ecase, edestruct et einduction (expérimental).	herbelin
2007-10-02	Correcting error message when adding Setoid, Relation or morphism (bug #1626)	jforest
2007-09-30	Suite de 10157	herbelin
2007-09-30	Ajout infos de débogage de "universe inconsistency" quand option Set	herbelin
2007-09-28	On empêche "fresh" d'engendrer un mot-clé.	herbelin
2007-09-27	Découpage de Setoid.v	notin
2007-09-21	- Fixing bug 1703 ("intros until n" falls back on the variable name when	herbelin
2007-09-17	Raffinement de l'algorithme d'inférence de type	herbelin
2007-09-06	Uniformisation politique de nommage evd/isevars (evd si evar_defs,	herbelin
2007-08-22	Correction du bug #1634 + ajout de bugs dans la test-suite	notin
2007-08-16	Correction du bug #1322	notin
2007-08-16	Correction du bug #1680: ajout d'un champ avoid_ids dans interp_sign;	notin
2007-08-07	Add a new tactic to generalize an instantiated inductive predicate adding equ...	msozeau
2007-07-24	Declarative language: fixed the generation of fixpoints for induction proofs.	corbinea
2007-07-18	Raffinement de interp_ident pour que l'ident interprété soit au choix	herbelin
2007-07-11	Slight cleanup of refl_omega.ml : in particular it uses now list	letouzey
2007-07-06	Adding a syntax for "n-ary" rewrite:	letouzey
2007-07-06	extension of the rename tactic: the following is now allowed:	letouzey
2007-07-06	New intro pattern "@A", which generates a fresh name based on A.	glondu
2007-06-26	killing some more non-exhaustive patterns	letouzey
2007-06-20	ajout de head0 et tail0 en natif	bgregoir
2007-05-29	Correction d'un bug dans l'affichage du message d'erreur real_clean	herbelin
2007-05-28	Contrôle de la compatibilité de apply via une information dans les	herbelin
2007-05-28	Retour à un message d'erreur d'apply qui montre un échec sans sans réduction	herbelin
2007-05-23	A fix for bug #1397:	letouzey
2007-05-22	Nouvelle stratégie d'unification des types des with-bindings dans	herbelin
2007-05-20	- Propagation des evars non résolues vers les with_bindings; permet par exemple	herbelin
2007-05-19	Backtrack sur l'effacement dans le contexte de but des lieurs	herbelin
2007-05-18	Interprétation des listes de VarArgType dans les notations faisant	herbelin
2007-05-18	Wish #1582 (3eme)	herbelin
2007-05-18	Quelques essais autour du wish implicite au rapport de bug #1582 (2eme)	herbelin
2007-05-18	Quelques essais autour du wish implicite au rapport de bug #1582	herbelin
2007-05-17	correction de bug dans Function et augmentation de la classe des fonctions su...	jforest
2007-05-17	Correction des bugs #1537 (anomalie sur signature incomplète) et #1536	herbelin
2007-05-11	Processor integers + Print assumption (see coqdev mailing list for the	aspiwack
2007-04-29	Multiples changements autour des implicites :	herbelin
2007-04-28	Ajout de la possibilité de faire référence dans certains cas à un nom	herbelin
2007-04-28	Ajout de la possibilité d'utiliser les evars dans apply_in et elim_in.	herbelin
2007-04-27	fixed glitch in escape	corbinea
2007-04-26	fin des conclusions multiples	corbinea
2007-04-25	New keyword "Inline" for Parameters and Axioms for automatic	soubiran
2007-04-18	debug plus poussé induction dépendante	corbinea
2007-04-18	- Correction d'un bug de make_clenv_binding_apply révélé par le commit 9771	herbelin
2007-04-16	Export de simplest_eapply, utilisé dans la contrib interface	notin
2007-04-16	fix bug with dependent inductive families	corbinea
2007-04-16	Suite unification apply et eapply (l'un et l'autre profite maintenant	herbelin
2007-04-15	Essai de partage de code entre apply et eapply	herbelin
2007-04-13	Proposition de correction pour le bug #1173 (ou du moins pour un	herbelin
2007-04-13	Nettoyage des tactiques basées sur "simpl" (delta-réduction cachant	herbelin