diff options
| author |  Ralf Jung <post@ralfj.de> | 2017-02-14 12:35:39 +0100 |
|---|---|---|
| committer | Ralf Jung <post@ralfj.de> | 2017-02-16 16:46:41 +0100 |
| commit | 55cb913f029308e97bd262fc18d4338f404e7561 (patch) | |
| tree | 3152c0912430102a15f1a22e5d69631431d92961 /parsing/pcoq.ml | |
| parent | 29d7872c0159d2aab7264c0577a2f5a9dc7c90c9 (diff) | |
don't require printing-only notation to be productive
Diffstat (limited to 'parsing/pcoq.ml')
| -rw-r--r-- | parsing/pcoq.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index 7dc02190e..007a6c767 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -267,6 +267,7 @@ module Prim = let integer = gec_gen "integer" let bigint = Gram.entry_create "Prim.bigint" let string = gec_gen "string" + let lstring = Gram.entry_create "Prim.lstring" let reference = make_gen_entry uprim "reference" let by_notation = Gram.entry_create "by_notation" let smart_global = Gram.entry_create "smart_global" |