From 55cb913f029308e97bd262fc18d4338f404e7561 Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Tue, 14 Feb 2017 12:35:39 +0100 Subject: don't require printing-only notation to be productive --- parsing/pcoq.mli | 1 + 1 file changed, 1 insertion(+) (limited to 'parsing/pcoq.mli') 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 -- cgit v1.2.3