diff options
| author | herbelin | 2002-11-25 12:24:43 +0000 |
|---|---|---|
| committer | herbelin | 2002-11-25 12:24:43 +0000 |
| commit | 95477bc8750375047d0c86dfbfda41ed221cac3c (patch) | |
| tree | 898a1e2e8e4e68287b7b72993d2e842b38d9b698 | |
| parent | 51bf8ac5bc08bf9acd131c17c025c6ed6960ab89 (diff) | |
Syntaxe delimiteurs
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3283 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | toplevel/metasyntax.ml | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index 8efa576f0d..29324cb5fa 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -664,12 +664,11 @@ let (inDelim,outDelim) = let make_delimiter_rule key typ = let e = Nameops.make_ident "e" None in - let m = key^":" in - let symbols = [Terminal "`"; Terminal m; NonTerminal e; Terminal "`"] in + let symbols = [Terminal ("'"^key^":"); NonTerminal e; Terminal "'"] in make_production [e,typ] symbols let add_delimiters scope key = let gram_rule = make_delimiter_rule key (ETConstr ((0,E),Some 0)) in let pat_gram_rule = make_delimiter_rule key ETPattern in - let dlms = ("`"^key^":", "`") in + let dlms = ("'"^key^":", "'") in Lib.add_anonymous_leaf (inDelim(gram_rule,pat_gram_rule,scope,dlms)) |