aboutsummaryrefslogtreecommitdiff
path: root/theories
AgeCommit message (Collapse)Author
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
2003-03-31Notation eqT superflueherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3816 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-29eq fusionne avec eqT et devient par défaut sur Type,herbelin
idem pour ex et exT, ex2 et exT2, all et allT git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3812 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-29Déplacement de minus dans Peanoherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3810 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-29Implicit Variables Typeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3809 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-28Pas d'associativité gauche au niveau 3 en vieille syntaxe !herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3803 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-28notations <>, Assumption avec existentiel, replace termmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3802 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-21*** empty log message ***barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3783 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-14*** empty log message ***barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3770 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-12*** empty log message ***barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3761 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-02-27Restructuration des hints pour qu'Auto fasse moins de détours et lesherbelin
preuves soient plus naturelles. En particulier, tentative de ramener systématiquement > et >= vers < et <=. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3708 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-02-14Ajout du theoreme de Cesarodesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3681 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-02-13Modifications dans une tactique topleveldelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3678 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-30Pb de parenthèse dans "Check (S (plus O O))"herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3632 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-28MAJ pour Regdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3615 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-22Documentation du contenu de REALSdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3594 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-22Modifications dans SeqPropdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3590 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-22Renommages dans Rtrigo_defdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3589 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-22Commentairesdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3587 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-22Renommages nombreuxdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3586 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-22Commentairesdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3585 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-22Renommage f_pos -> IVT (Intermediate Value Theoremdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3583 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-22Suppression d'un Import R_scope probablement oubliedesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3582 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-22Commentairesdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3581 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-22Renommages dans RListdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3580 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-22MAJ pour renommage Rcompletdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3579 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-22Renommages dans Rcompletedesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3578 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-22Renommage Rcomplet.v -> Rcomplete.vdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3577 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-22Suppression de lemmes superflusdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3576 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-22Commentairesdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3575 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-22Renommages dans PartSumdesmettr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3574 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-22Bug precedenceherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3572 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-01 00:25:53 +0000