aboutsummaryrefslogtreecommitdiff
path: root/theories/Logic
AgeCommit message (Expand)Author
2003-11-02Renommage bool en boolP pour eviter la qualificationherbelin
2003-10-29Choix sous sa forme relationnelleherbelin
2003-10-28MAJherbelin
2003-10-28Fichier offrant l'axiome du choix unique en presence de logique classiqueherbelin
2003-10-28Fichier offrant l'axiome du choix en presence de logique classiqueherbelin
2003-10-28La logique sur Type inclut celle sur Setherbelin
2003-10-03Cacher les .v8herbelin
2003-04-29Ajout ChoiceFactsherbelin
2003-04-29Blancsherbelin
2003-04-09Renommage K; equivalence JMeq et eq_dep sur Typeherbelin
2003-04-03Documentation, généralisation à eq sur Type, preuves d'équivalence desherbelin
2002-11-14JMeq now treated as an equality by tactics.courant
2002-08-13Preuves dans CC deherbelin
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-03-02 09:36:05 +0000