aboutsummaryrefslogtreecommitdiffhomepage
path: root/grammar/q_constr.ml4
diff options
context:
space:
mode:
Diffstat (limited to 'grammar/q_constr.ml4')
-rw-r--r--grammar/q_constr.ml42
1 files changed, 1 insertions, 1 deletions
diff --git a/grammar/q_constr.ml4 b/grammar/q_constr.ml4
index cf671adcb..e1db0a05a 100644
--- a/grammar/q_constr.ml4
+++ b/grammar/q_constr.ml4
@@ -30,7 +30,7 @@ EXTEND
sort:
[ [ "Set" -> Misctypes.GSet
| "Prop" -> Misctypes.GProp
- | "Type" -> Misctypes.GType None ] ]
+ | "Type" -> Misctypes.GType [] ] ]
;
ident:
[ [ s = string -> <:expr< Names.Id.of_string $str:s$ >> ] ]