diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2014-09-08 10:23:12 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2014-09-08 17:09:43 +0200 |
| commit | 26a79004e47bbdc97df61015ce7e944eef14ac71 (patch) | |
| tree | 1f24c9acbb73cd63dcc689222b965f245767137e /grammar/q_constr.ml4 | |
| parent | 89ad50f4d7e1312539995ced3a632821bf6af7c5 (diff) | |
Parsing of Type@{max(i,j)}.
Diffstat (limited to 'grammar/q_constr.ml4')
| -rw-r--r-- | grammar/q_constr.ml4 | 2 |
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$ >> ] ] |