aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/g_prim.ml4
Commit message (Collapse)AuthorAge
...
* Nouveau lexeme METAIDENT pour les $idGravatar herbelin2000-11-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@890 85f007b7-540e-0410-9357-904b9bb8a0f7
* Changement/extension dans les noms de parseurs de GrammarGravatar herbelin2000-11-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@814 85f007b7-540e-0410-9357-904b9bb8a0f7
* compilation des fichiers ml4 sans GNUseriesGravatar filliatr2000-11-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@795 85f007b7-540e-0410-9357-904b9bb8a0f7
* Parsing des motifs de Syntax avec la grammaire associée à l'univers de la ↵Gravatar herbelin2000-10-18
| | | | | | déclaration (constr, tactic ou vernac) au lieu de ast (comme cela a été fait pour Grammar) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@721 85f007b7-540e-0410-9357-904b9bb8a0f7
* Plus de piquants dans les actions des grammaires; nom de la grammaire pris ↵Gravatar herbelin2000-07-28
| | | | | | comme parseur par defaut; le type List devient AstList git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@575 85f007b7-540e-0410-9357-904b9bb8a0f7
* compilation des grammaires (ouf)Gravatar filliatr1999-09-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@57 85f007b7-540e-0410-9357-904b9bb8a0f7
* modules grammaire CoqGravatar filliatr1999-09-08
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@55 85f007b7-540e-0410-9357-904b9bb8a0f7