aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/q_constr.ml4
diff options
context:
space:
mode:
Diffstat (limited to 'parsing/q_constr.ml4')
-rw-r--r--parsing/q_constr.ml44
1 files changed, 3 insertions, 1 deletions
diff --git a/parsing/q_constr.ml4 b/parsing/q_constr.ml4
index 4c86e4415..fb34a5aa2 100644
--- a/parsing/q_constr.ml4
+++ b/parsing/q_constr.ml4
@@ -12,7 +12,9 @@ open Names
open Pattern
open Q_util
open Util
+open Compat
open Pcaml
+open PcamlSig
let loc = dummy_loc
let dloc = <:expr< Util.dummy_loc >>
@@ -40,7 +42,7 @@ EXTEND
[ [ "_" -> <:expr< Anonymous >> | id = ident -> <:expr< Name $id$ >> ] ]
;
string:
- [ [ UIDENT | LIDENT ] ]
+ [ [ s = UIDENT -> s | s = LIDENT -> s ] ]
;
constr:
[ "200" RIGHTA