diff options
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_vernac.ml4 | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 5fe558adf1..c9700cdf01 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -378,10 +378,11 @@ GEXTEND Gram ; of_type_with_opt_coercion: [ [ ":>>" -> Some false - | ":>" -> Some true - | ":"; ">" -> Some true - | ":"; ">"; ">" -> Some false - | ":" -> None ] ] + | ":>"; ">" -> Some false + | ":>" -> Some true + | ":"; ">"; ">" -> Some false + | ":"; ">" -> Some true + | ":" -> None ] ] ; END |