aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc
Commit message (Collapse)AuthorAge
* Nettoyage et documentation de LibraryGravatar herbelin2005-02-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6692 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2005-01-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6623 85f007b7-540e-0410-9357-904b9bb8a0f7
* Tactic Notation et with-namesGravatar herbelin2004-03-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5416 85f007b7-540e-0410-9357-904b9bb8a0f7
* - fixed the Assert_failure error in kernel/modopsGravatar barras2004-02-18
| | | | | | | | | - fixed the problem with passing atomic tactics to ltacs - restructured the distrib Makefile (can build a package from the CVS working dir) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5358 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression de 'Print.' en v8Gravatar herbelin2004-01-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5265 85f007b7-540e-0410-9357-904b9bb8a0f7
* bugs avec Pose et AssertGravatar barras2004-01-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5190 85f007b7-540e-0410-9357-904b9bb8a0f7
* *** empty log message ***Gravatar barras2003-12-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5147 85f007b7-540e-0410-9357-904b9bb8a0f7
* *** empty log message ***Gravatar barras2003-12-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5146 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJ NotationGravatar herbelin2003-12-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5143 85f007b7-540e-0410-9357-904b9bb8a0f7
* *** empty log message ***Gravatar barras2003-12-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5134 85f007b7-540e-0410-9357-904b9bb8a0f7
* modif existentielle (exists | --> exists ,) + bug d'affichage des pt fixesGravatar barras2003-12-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5099 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJ 'abstract'Gravatar herbelin2003-12-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5067 85f007b7-540e-0410-9357-904b9bb8a0f7
* Reparation bug compilGravatar mohring2003-11-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5005 85f007b7-540e-0410-9357-904b9bb8a0f7
* modif lexer: ident peut commencer par _Gravatar barras2003-11-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4991 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJsGravatar herbelin2003-11-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4975 85f007b7-540e-0410-9357-904b9bb8a0f7
* moins unaire au niveau 35, tactiques simple_induction et simple_destruct, ↵Gravatar barras2003-11-13
| | | | | | Local devient Let git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4897 85f007b7-540e-0410-9357-904b9bb8a0f7
* factorisation et generalisation des clausesGravatar barras2003-11-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4892 85f007b7-540e-0410-9357-904b9bb8a0f7
* petits changements de syntaxeGravatar barras2003-11-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4860 85f007b7-540e-0410-9357-904b9bb8a0f7
* 'as' avant 'using' dans 'destruct'Gravatar herbelin2003-11-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4838 85f007b7-540e-0410-9357-904b9bb8a0f7
* OubliGravatar herbelin2003-11-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4814 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2003-11-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4813 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2003-11-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4800 85f007b7-540e-0410-9357-904b9bb8a0f7
* *** empty log message ***Gravatar barras2003-11-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4793 85f007b7-540e-0410-9357-904b9bb8a0f7
* nouvelles priorites + HintsGravatar barras2003-10-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4695 85f007b7-540e-0410-9357-904b9bb8a0f7
* *** empty log message ***Gravatar barras2003-10-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4685 85f007b7-540e-0410-9357-904b9bb8a0f7
* *** empty log message ***Gravatar barras2003-10-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4675 85f007b7-540e-0410-9357-904b9bb8a0f7
* nouvelle syntaxe de ltacGravatar barras2003-10-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4661 85f007b7-540e-0410-9357-904b9bb8a0f7
* lettac -> setGravatar barras2003-10-16
| | | | | | | suppression de la notation carre de R git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4659 85f007b7-540e-0410-9357-904b9bb8a0f7
* *** empty log message ***Gravatar barras2003-10-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4657 85f007b7-540e-0410-9357-904b9bb8a0f7
* mise a jour nouvelle syntaxeGravatar barras2003-10-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4595 85f007b7-540e-0410-9357-904b9bb8a0f7
* *** empty log message ***Gravatar barras2003-10-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4518 85f007b7-540e-0410-9357-904b9bb8a0f7
* About, InfixGravatar herbelin2003-09-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4486 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2003-09-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4448 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout nouvelles commandesGravatar herbelin2003-09-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4389 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2003-09-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4325 85f007b7-540e-0410-9357-904b9bb8a0f7
* Relachement conflit 'with' dans le cas des Module with DefinitionGravatar herbelin2003-09-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4295 85f007b7-540e-0410-9357-904b9bb8a0f7
* Syntaxe des constructeurs et des hypothesesGravatar herbelin2003-08-31
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4286 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2003-08-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4258 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added new syntax definitionGravatar barras2003-06-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4100 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
* exemple complet de parserGravatar barras2002-12-17
| | | | | | | | changement de syntaxe des scope: expr % id ex: (10 + 5 * 4)%N ou 4%N git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3451 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJ travail moulinetteGravatar herbelin2002-12-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3368 85f007b7-540e-0410-9357-904b9bb8a0f7
* pseudo-parser ocamlyacc de la nouvelle syntaxeGravatar barras2002-11-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3303 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
* MoulinetteGravatar herbelin2002-11-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3202 85f007b7-540e-0410-9357-904b9bb8a0f7
* DiversGravatar herbelin2002-11-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3201 85f007b7-540e-0410-9357-904b9bb8a0f7
* BugsGravatar herbelin2002-10-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3195 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout d'infixesGravatar herbelin2002-10-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3158 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modules dans COQ\!\!\!\!Gravatar coq2002-08-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2957 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et ↵Gravatar herbelin2002-05-29
| | | | | | commandes vernaculaires (cf dev/changements.txt pour plus de précisions) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2734 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-20 16:26:55 +0000