diff options
| author | herbelin | 2000-11-20 09:05:35 +0000 |
|---|---|---|
| committer | herbelin | 2000-11-20 09:05:35 +0000 |
| commit | 125c2ade92dbdd891c86850e9710a1f203c4ec3c (patch) | |
| tree | 43ef5ade84f1f78703d07bf58d81bafa49b66cdf | |
| parent | 01d00e2f27b4434076d58d3bcf6598ea3af34e3c (diff) | |
Prise en compte des noms qualifiés dans certaines commandes
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@891 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | parsing/g_vernac.ml4 | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index a3145ca04d..0a7c0586b3 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -310,9 +310,9 @@ GEXTEND Gram | IDENT "End"; id = identarg; "." -> <:ast< (EndSection $id) >> (* Transparent and Opaque *) - | IDENT "Transparent"; l = ne_identarg_list; "." -> + | IDENT "Transparent"; l = ne_qualidconstarg_list; "." -> <:ast< (TRANSPARENT ($LIST $l)) >> - | IDENT "Opaque"; l = ne_identarg_list; "." -> + | IDENT "Opaque"; l = ne_qualidconstarg_list; "." -> <:ast< (OPAQUE ($LIST $l)) >> (* Coercions *) |