aboutsummaryrefslogtreecommitdiffhomepage
path: root/CHANGES
Commit message (Collapse)AuthorAge
* MAJGravatar herbelin2003-11-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4864 85f007b7-540e-0410-9357-904b9bb8a0f7
* deux doigts d'extraction dans le CHANGES pour la V8Gravatar letouzey2003-11-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4859 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2003-11-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4831 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2003-10-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4739 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2003-10-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4619 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2003-10-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4582 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2003-10-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4544 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2003-09-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4489 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout option Local à Hint, Hints et HintDestructGravatar herbelin2003-06-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4163 85f007b7-540e-0410-9357-904b9bb8a0f7
* Utilisation de intro_pattern dans NewDestruct/NewInductionGravatar herbelin2003-06-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4154 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2003-06-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4135 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout FreshIdGravatar herbelin2003-05-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4072 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2003-05-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4048 85f007b7-540e-0410-9357-904b9bb8a0f7
* ajout d'une elimination simplifiée Acc_iter pour AccGravatar letouzey2003-04-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3966 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2003-04-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3944 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2003-04-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3885 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2003-03-31
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3830 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
* Mise en place de 'Implicit Variable' (variante du 'Reserve' de mizar)Gravatar herbelin2003-03-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3807 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout de Set Print WidthGravatar gregoire2003-03-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3790 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2003-02-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3717 85f007b7-540e-0410-9357-904b9bb8a0f7
* Chargement dynamique de .cmaGravatar delahaye2003-02-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3676 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug RenameGravatar herbelin2003-02-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3671 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2003-02-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3668 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2003-02-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3658 85f007b7-540e-0410-9357-904b9bb8a0f7
* release 7.4; changement magic numberGravatar filliatr2003-02-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3652 85f007b7-540e-0410-9357-904b9bb8a0f7
* maj status de l'extraction des modulesGravatar letouzey2003-02-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3649 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2003-01-31
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3641 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2003-01-31
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3640 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2003-01-31
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3639 85f007b7-540e-0410-9357-904b9bb8a0f7
* *** empty log message ***Gravatar courant2003-01-31
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3636 85f007b7-540e-0410-9357-904b9bb8a0f7
* status de l'extractionGravatar letouzey2003-01-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3600 85f007b7-540e-0410-9357-904b9bb8a0f7
* Changements dans REALSGravatar desmettr2003-01-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3592 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2003-01-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3541 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJ LtacGravatar herbelin2003-01-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3536 85f007b7-540e-0410-9357-904b9bb8a0f7
* V7.4Gravatar mohring2003-01-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3524 85f007b7-540e-0410-9357-904b9bb8a0f7
* Mise a jour pour distribGravatar mohring2003-01-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3521 85f007b7-540e-0410-9357-904b9bb8a0f7
* *** empty log message ***Gravatar mohring2003-01-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3520 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug en présence de let-inGravatar herbelin2003-01-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3502 85f007b7-540e-0410-9357-904b9bb8a0f7
* Prise en compte des coercions dans les 'with' bindingsGravatar herbelin2002-12-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3468 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2002-12-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3446 85f007b7-540e-0410-9357-904b9bb8a0f7
* *** empty log message ***Gravatar gregoire2002-12-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3426 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout Simpl et Change sur des sous-termesGravatar herbelin2002-12-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3399 85f007b7-540e-0410-9357-904b9bb8a0f7
* Amélioration sensible de l'efficacité de Zmult et timesGravatar herbelin2002-12-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3385 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2002-12-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3364 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout des options "Set Contextual Implicits" et "Set Strict ImplicitsGravatar herbelin2002-12-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3353 85f007b7-540e-0410-9357-904b9bb8a0f7
* Utilisation des niveaux de camlp4 pour gérer les niveaux de constr; ↵Gravatar herbelin2002-11-24
| | | | | | améliorations diverses de l'affichage; affinement de la syntaxe et des options de Notation; branchement de Syntactic Definition sur Notation git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3270 85f007b7-540e-0410-9357-904b9bb8a0f7
* Réforme de l'interprétation des termes :Gravatar herbelin2002-11-14
| | | | | | | | | | | | | | | - Le parsing se fait maintenant via "constr_expr" au lieu de "Coqast.t" - "Coqast.t" reste pour l'instant pour le pretty-printing. Un deuxième pretty-printer dans ppconstr.ml est basé sur "constr_expr". - Nouveau répertoire "interp" qui hérite de la partie interprétation qui se trouvait avant dans "parsing" (constrintern.ml remplace astterm.ml; constrextern.ml est l'équivalent de termast.ml pour le nouveau printer; topconstr.ml; contient la définition de "constr_expr"; modintern.ml remplace astmod.ml) - Libnames.reference tend à remplacer Libnames.qualid git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3235 85f007b7-540e-0410-9357-904b9bb8a0f7
* Des critères plus fins d'analyse des implicites automatiques; meilleur ↵Gravatar herbelin2002-10-28
| | | | | | affichage des implicites en cas d'application partielle ou inférence via une position flexible; gestion des implicites en positions terminales pour anticiper sur un implicite dans nil et cie git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3185 85f007b7-540e-0410-9357-904b9bb8a0f7
* Clarification changements autour de Remark/Fact/LocalGravatar herbelin2002-10-23
| | | | | | | Ajout de la syntaxe "Theorem f [binders] : t", comme pour Definition et Local git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3180 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-07 03:54:00 +0000