diff options
author | 2000-11-07 10:47:25 +0000 | |
---|---|---|
committer | 2000-11-07 10:47:25 +0000 | |
commit | c803556c297d40d96e6730ab334b5b7e826f4d77 (patch) | |
tree | aa118c4bca829b630aef51796fbbc9cf40003c2d /CHANGES | |
parent | 30de194fa897bb44858c92dd458041bb2d2df9fe (diff) |
Changement/extension dans les noms de parseurs de Grammar
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@814 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'CHANGES')
-rw-r--r-- | CHANGES | 8 |
1 files changed, 5 insertions, 3 deletions
@@ -35,9 +35,11 @@ commandes) motifs des règles d'affichage est maintenant celui associé au nom de la grammaire (vernac, tactic ou constr). Donc plus de piquants <:vernac:<...>> etc. Pour retourner de l'ast, il faut typer -explicitement la grammaire avec Ast ou List (renommé d'ailleurs -AstList), ou, si c'est dans une règle Syntax, utiliser la quotation -<< ... >> qui replace dans ast. +explicitement la grammaire avec "ast" ou "List" (renommé d'ailleurs +"ast list"), ou, si c'est dans une règle Syntax, utiliser la quotation +<< ... >> qui replace dans ast. Pour les nouvelles grammaires (autre +que les 3 primitives), on peut typer avec "constr", "tactic", ou +"vernac" pour utiliser le parseur correspondant. - AddPath -> Add Path; Print LoadPath -> Print Path; |