aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/metasyntax.mli
Commit message (Collapse)AuthorAge
...
* Déplacement de qualid dans Nametab, hors du noyauGravatar herbelin2001-03-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1419 85f007b7-540e-0410-9357-904b9bb8a0f7
* syntaxe AST Inversion + commentaires ocamlweb autour de $Gravatar filliatr2000-12-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1090 85f007b7-540e-0410-9357-904b9bb8a0f7
* Abstraction du type 'qualid' pour les noms qualifiés relatifs distinct de ↵Gravatar herbelin2000-11-22
| | | | | | 'section_path' pour les noms absolus git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@919 85f007b7-540e-0410-9357-904b9bb8a0f7
* Prise en compte noms longsGravatar herbelin2000-11-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@857 85f007b7-540e-0410-9357-904b9bb8a0f7
* module MetasyntaxGravatar filliatr1999-12-01
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@177 85f007b7-540e-0410-9357-904b9bb8a0f7