aboutsummaryrefslogtreecommitdiff
path: root/theories
AgeCommit message (Collapse)Author
2003-05-22Ajout V8Notationherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4061 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-21Concentration des notations officielles dans Init/Notations; restructuration ↵herbelin
de Init git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4050 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-21Notationsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4047 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-21Bugherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4046 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-14Amelioration presentationherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4020 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-14Amelioration affichageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4019 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-14Suppression de 'R' dans la notation == entreherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4016 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-14Suppression de 'R' dans la notation == entreherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4015 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-14Deplacement lemmes sur fact de Reals vers Arithherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4014 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-13Nouveaux lemmesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4013 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-13Nouveaux lemmes (sur proposition de Nijmegen)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4012 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-13Nouveaux lemmes (sur proposition de Nijmegen)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4010 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-09ajout inverse relation bien fondeemohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4000 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-07coqide: toolbar/autosavemonate
Hugo: Suppression du type dans les notations == et <> entre git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3992 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-29Blancsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3980 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-29Notationsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3979 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-29Implicit Typesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3978 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-29Ajout ChoiceFactsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3977 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-29Blancsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3976 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-29En v8: abandon de Rle_sym2, Rle_sym1 au profit de Rge_le, Rle_ge; abandon de ↵herbelin
Rlt_sym, Rle_sym; utilisation de la terminologie 'commutative' plutôt que 'symétrie' pour les opérateurs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3972 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-28Un principe light d'elimination de Acc, suivant les remarques de Yves Bertotletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3964 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-17Intégration DatatypesSyntax à Datatypesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3945 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-17Diversherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3943 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-17<> maintenant standardherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3942 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-17Intégration DatatypesSyntax à Datatypesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3941 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-17Syntaxe 'x=y:>T'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3940 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-16suite au commit d'hugo dans TypeSyntax & Raxiom, Intro donnait un nom differentletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3933 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-16sumboolT, sumorT, sigTT, SigT redondantsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3927 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-14Cosmetiqueherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3923 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-14Local 'o'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3918 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-12Open Scope en Localherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3917 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-10Open Scope remplace Importherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3912 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-10Calcul automatique de l'implicite de nil pour que l'affichage sache le traiterherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3911 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-10Remplacement Import par Open Scope en v8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3909 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-09cast de nilherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3897 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-09nil en implicite dans la v8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3895 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-09Ajout Open Scopeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3890 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-09Activation des implicites pour la v8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3886 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-09Suppression de l'étage "Import nat/Z/R_scope". "Open Scope" remplace "Import"herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3881 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-09Renommage K; equivalence JMeq et eq_dep sur Typeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3879 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-09Definedherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3878 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-09Suppression de l'étage "Import nat/Z/R_scope". "Open Scope" remplace "Import".herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3877 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-09Suppression de l'étage "Import nat/Z/R_scope". "Open Scope" remplace "Import"herbelin
Expérience avec les notations et les scopes git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3876 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-07Nommage explicite des hypotheses introduites quand le nom existe aussi comme ↵herbelin
global git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3861 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-07Cosmetiqueherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3855 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-07Espaces superflusherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3853 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-03Documentation, généralisation à eq sur Type, preuves d'équivalence desherbelin
4 axiomes (K, UIP, eq_rec_eq, eq_dep_eq) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3843 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-31Ajout double_plusherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3828 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-31Ajout Implicit Variable Typeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3827 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-31Suppression des alias eqT/exT/exT2 en nouvelle syntaxeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3821 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-10-08 02:12:00 +0000