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.mli | |
parent | 29d7872c0159d2aab7264c0577a2f5a9dc7c90c9 (diff) |
don't require printing-only notation to be productive
Diffstat (limited to 'parsing/pcoq.mli')
-rw-r--r-- | parsing/pcoq.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 37165f6ce..fc1727fc1 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -137,6 +137,7 @@ module Prim : val bigint : Bigint.bigint Gram.entry val integer : int Gram.entry val string : string Gram.entry + val lstring : string located Gram.entry val qualid : qualid located Gram.entry val fullyqualid : Id.t list located Gram.entry val reference : reference Gram.entry |