diff options
Diffstat (limited to 'parsing/g_vernac.ml4')
| -rw-r--r-- | parsing/g_vernac.ml4 | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index b7b9e2a6a..b5e9f9e06 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -189,7 +189,7 @@ let test_plural_form_types = function (* Gallina declarations *) GEXTEND Gram GLOBAL: gallina gallina_ext thm_token def_body of_type_with_opt_coercion - record_field decl_notation rec_definition; + record_field decl_notation rec_definition pidentref; gallina: (* Definition, Theorem, Variable, Axiom, ... *) @@ -780,10 +780,10 @@ GEXTEND Gram | IDENT "transparent" -> Conv_oracle.transparent ] ] ; instance_name: - [ [ name = identref; sup = OPT binders -> - (let (loc,id) = name in (loc, Name id)), + [ [ name = pidentref; sup = OPT binders -> + (let ((loc,id),l) = name in ((loc, Name id),l)), (Option.default [] sup) - | -> (!@loc, Anonymous), [] ] ] + | -> ((!@loc, Anonymous), None), [] ] ] ; reserv_list: [ [ bl = LIST1 reserv_tuple -> bl | b = simple_reserv -> [b] ] ] |