aboutsummaryrefslogtreecommitdiff
path: root/theories/Logic
AgeCommit message (Expand)Author
2002-05-29Ajout Hurkens.v, ProofIrrelevances.v et l'indiscernabilite dans Classical_Prop.vherbelin
2002-04-17Uniformisation (Qed/Save et Implicits Arguments)herbelin
2002-03-26Prise en compte des dependances dans la tactique Casemohring
2002-02-14option -dump-glob pour coqdocfilliatr
2001-08-13Protection des commentaires pour coqtex et coqwebherbelin
2001-08-05Expérimentation de NewDestruct et parfois NewInductionherbelin
2001-06-18Ajout du paradoxe de Berardi dans Logic (preuve que EM => PI dans CCI)barras
2001-04-19Mise de (*i autour CVS infomohring
2001-04-12Ajout de l'egalite de John Majormohring
2001-04-11documentation automatique de la bibliothèque standardfilliatr
2001-04-08Ajout lemmes arithmetiquesmohring
2001-03-15entetesfilliatr
2001-02-14Renommage des variables dans les schémas d'inductionherbelin
2000-12-04caractere opaque des constantes repris en comptefilliatr
2000-10-06Un usage en moins de l'axiome eq_rec_eqherbelin
2000-10-04Commit malencontreux sur précédente versionherbelin
2000-10-04Mise en conformité nouveau Simpl pour Fixherbelin
2000-03-21Eqdep_dec retrouve ses noms d'origine grace au nouvel Reduction.instance util...herbelin
2000-03-16Syntactic Definition n'etaient pas correctemenet importeesfilliatr
2000-03-10*** empty log message ***barras
2000-01-21gros commit de tout ce que j'ai fait pendant les vacances :filliatr
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-15 20:02:20 +0000