aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Logic
Commit message (Expand)AuthorAge
* add a left and right tactic for classical logicGravatar narboux2005-07-15
* MAJ changements ChoiceFactsGravatar herbelin2004-12-05
* Paramétrisation du domaine des axiomes de choix + ajout description = choice...Gravatar herbelin2004-12-05
* MAJ commentaire sur incohérence EM dans SetGravatar herbelin2004-11-07
* Réponse à la conjecture que PI est indépendant de EM dans CCGravatar herbelin2004-11-02
* Minimisation utilisation NNPPGravatar herbelin2004-08-03
* Déclaration d'obsolescenceGravatar herbelin2004-08-03
* TypoGravatar herbelin2004-08-03
* RefGravatar herbelin2004-08-03
* Commentaires coqdocGravatar herbelin2004-08-01
* Commentaires coqdocGravatar herbelin2004-08-01
* Nouvelle en-têteGravatar herbelin2004-07-16
* simplified proof (eq and eqT are now the same)Gravatar barras2004-06-25
* eq2eqT et eqT2eq devenus obsolètesGravatar herbelin2004-06-02
* MAJ commentairesGravatar herbelin2004-03-24
* CommentairesGravatar herbelin2004-03-17
* MAJ simplificationGravatar herbelin2004-01-27
* changement de pose en set (pose n'etait pas utilise avec la semantiqueGravatar barras2003-12-24
* modif existentielle (exists | --> exists ,) + bug d'affichage des pt fixesGravatar barras2003-12-15
* Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ...Gravatar herbelin2003-11-29
* Biblio standard sans mention de la possibilite d'etre impredicatifGravatar herbelin2003-11-07
* Biblio standard sans impredicativiteGravatar herbelin2003-11-07
* Preuve de l'incoherence de {A}+{~A} avec Set impredicatifGravatar herbelin2003-11-05
* CosmetiqueGravatar herbelin2003-11-02
* Renforcement significatif du resultat principalGravatar herbelin2003-11-02
* Rien de bien importantGravatar herbelin2003-11-02
* CommentairesGravatar herbelin2003-11-02
* TypoGravatar herbelin2003-11-02
* AC + EXT -> EMGravatar herbelin2003-11-02
* Relations entre le choix (forme relationnelle) avec restriction ou nonGravatar herbelin2003-11-02
* Renommage bool en boolP pour eviter la qualificationGravatar herbelin2003-11-02
* Choix sous sa forme relationnelleGravatar herbelin2003-10-29
* MAJGravatar herbelin2003-10-28
* Fichier offrant l'axiome du choix unique en presence de logique classiqueGravatar herbelin2003-10-28
* Fichier offrant l'axiome du choix en presence de logique classiqueGravatar herbelin2003-10-28
* La logique sur Type inclut celle sur SetGravatar herbelin2003-10-28
* Cacher les .v8Gravatar herbelin2003-10-03
* Ajout ChoiceFactsGravatar herbelin2003-04-29
* BlancsGravatar herbelin2003-04-29
* Renommage K; equivalence JMeq et eq_dep sur TypeGravatar herbelin2003-04-09
* Documentation, généralisation à eq sur Type, preuves d'équivalence desGravatar herbelin2003-04-03
* JMeq now treated as an equality by tactics.Gravatar courant2002-11-14
* Preuves dans CC deGravatar herbelin2002-08-13
* Ajout Hurkens.v, ProofIrrelevances.v et l'indiscernabilite dans Classical_Prop.vGravatar herbelin2002-05-29
* Uniformisation (Qed/Save et Implicits Arguments)Gravatar herbelin2002-04-17
* Prise en compte des dependances dans la tactique CaseGravatar mohring2002-03-26
* option -dump-glob pour coqdocGravatar filliatr2002-02-14
* Protection des commentaires pour coqtex et coqwebGravatar herbelin2001-08-13
* Expérimentation de NewDestruct et parfois NewInductionGravatar herbelin2001-08-05
* Ajout du paradoxe de Berardi dans Logic (preuve que EM => PI dans CCI)Gravatar barras2001-06-18
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-29 12:30:10 +0000