aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories
Commit message (Collapse)AuthorAge
* Remplacement Import par Open Scope en v8Gravatar herbelin2003-04-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3909 85f007b7-540e-0410-9357-904b9bb8a0f7
* cast de nilGravatar herbelin2003-04-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3897 85f007b7-540e-0410-9357-904b9bb8a0f7
* nil en implicite dans la v8Gravatar herbelin2003-04-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3895 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout Open ScopeGravatar herbelin2003-04-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3890 85f007b7-540e-0410-9357-904b9bb8a0f7
* Activation des implicites pour la v8Gravatar herbelin2003-04-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3886 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression de l'étage "Import nat/Z/R_scope". "Open Scope" remplace "Import"Gravatar herbelin2003-04-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3881 85f007b7-540e-0410-9357-904b9bb8a0f7
* Renommage K; equivalence JMeq et eq_dep sur TypeGravatar herbelin2003-04-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3879 85f007b7-540e-0410-9357-904b9bb8a0f7
* DefinedGravatar herbelin2003-04-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3878 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression de l'étage "Import nat/Z/R_scope". "Open Scope" remplace "Import".Gravatar herbelin2003-04-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3877 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression de l'étage "Import nat/Z/R_scope". "Open Scope" remplace "Import"Gravatar herbelin2003-04-09
| | | | | | | 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
* Nommage explicite des hypotheses introduites quand le nom existe aussi comme ↵Gravatar herbelin2003-04-07
| | | | | | global git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3861 85f007b7-540e-0410-9357-904b9bb8a0f7
* CosmetiqueGravatar herbelin2003-04-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3855 85f007b7-540e-0410-9357-904b9bb8a0f7
* Espaces superflusGravatar herbelin2003-04-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3853 85f007b7-540e-0410-9357-904b9bb8a0f7
* Documentation, généralisation à eq sur Type, preuves d'équivalence desGravatar herbelin2003-04-03
| | | | | | | 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
* Ajout double_plusGravatar herbelin2003-03-31
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3828 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout Implicit Variable TypeGravatar herbelin2003-03-31
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3827 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression des alias eqT/exT/exT2 en nouvelle syntaxeGravatar herbelin2003-03-31
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3821 85f007b7-540e-0410-9357-904b9bb8a0f7
* Notation eqT superflueGravatar herbelin2003-03-31
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3816 85f007b7-540e-0410-9357-904b9bb8a0f7
* eq fusionne avec eqT et devient par défaut sur Type,Gravatar herbelin2003-03-29
| | | | | | | 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
* Déplacement de minus dans PeanoGravatar herbelin2003-03-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3810 85f007b7-540e-0410-9357-904b9bb8a0f7
* Implicit Variables TypeGravatar herbelin2003-03-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3809 85f007b7-540e-0410-9357-904b9bb8a0f7
* Pas d'associativité gauche au niveau 3 en vieille syntaxe !Gravatar herbelin2003-03-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3803 85f007b7-540e-0410-9357-904b9bb8a0f7
* notations <>, Assumption avec existentiel, replace termGravatar mohring2003-03-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3802 85f007b7-540e-0410-9357-904b9bb8a0f7
* *** empty log message ***Gravatar barras2003-03-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3783 85f007b7-540e-0410-9357-904b9bb8a0f7
* *** empty log message ***Gravatar barras2003-03-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3770 85f007b7-540e-0410-9357-904b9bb8a0f7
* *** empty log message ***Gravatar barras2003-03-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3761 85f007b7-540e-0410-9357-904b9bb8a0f7
* Restructuration des hints pour qu'Auto fasse moins de détours et lesGravatar herbelin2003-02-27
| | | | | | | | 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
* Ajout du theoreme de CesaroGravatar desmettr2003-02-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3681 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modifications dans une tactique toplevelGravatar delahaye2003-02-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3678 85f007b7-540e-0410-9357-904b9bb8a0f7
* Pb de parenthèse dans "Check (S (plus O O))"Gravatar herbelin2003-01-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3632 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJ pour RegGravatar desmettr2003-01-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3615 85f007b7-540e-0410-9357-904b9bb8a0f7
* Documentation du contenu de REALSGravatar desmettr2003-01-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3594 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modifications dans SeqPropGravatar desmettr2003-01-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3590 85f007b7-540e-0410-9357-904b9bb8a0f7
* Renommages dans Rtrigo_defGravatar desmettr2003-01-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3589 85f007b7-540e-0410-9357-904b9bb8a0f7
* CommentairesGravatar desmettr2003-01-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3587 85f007b7-540e-0410-9357-904b9bb8a0f7
* Renommages nombreuxGravatar desmettr2003-01-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3586 85f007b7-540e-0410-9357-904b9bb8a0f7
* CommentairesGravatar desmettr2003-01-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3585 85f007b7-540e-0410-9357-904b9bb8a0f7
* Renommage f_pos -> IVT (Intermediate Value TheoremGravatar desmettr2003-01-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3583 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression d'un Import R_scope probablement oublieGravatar desmettr2003-01-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3582 85f007b7-540e-0410-9357-904b9bb8a0f7
* CommentairesGravatar desmettr2003-01-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3581 85f007b7-540e-0410-9357-904b9bb8a0f7
* Renommages dans RListGravatar desmettr2003-01-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3580 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJ pour renommage RcompletGravatar desmettr2003-01-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3579 85f007b7-540e-0410-9357-904b9bb8a0f7
* Renommages dans RcompleteGravatar desmettr2003-01-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3578 85f007b7-540e-0410-9357-904b9bb8a0f7
* Renommage Rcomplet.v -> Rcomplete.vGravatar desmettr2003-01-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3577 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression de lemmes superflusGravatar desmettr2003-01-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3576 85f007b7-540e-0410-9357-904b9bb8a0f7
* CommentairesGravatar desmettr2003-01-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3575 85f007b7-540e-0410-9357-904b9bb8a0f7
* Renommages dans PartSumGravatar desmettr2003-01-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3574 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug precedenceGravatar herbelin2003-01-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3572 85f007b7-540e-0410-9357-904b9bb8a0f7
* Adaptation à la nouvelle sémantique plus uniforme de "Match term"Gravatar herbelin2003-01-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3567 85f007b7-540e-0410-9357-904b9bb8a0f7
* Renommage dans MVTGravatar desmettr2003-01-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3564 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-08-13 09:41:47 +0000