diff options
| -rw-r--r-- | vernac/vernacentries.ml | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 6dfba02ae9..5956a2e600 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1048,8 +1048,8 @@ let vernac_identity_coercion ~atts id qids qidt = let vernac_instance_program ~atts name bl t props info = Dumpglob.dump_constraint (fst name) false "inst"; - let (program, locality), poly = - Attributes.(parse (Notations.(program ++ locality ++ polymorphic))) atts + let locality, poly = + Attributes.(parse (Notations.(locality ++ polymorphic))) atts in let global = not (make_section_locality locality) in let _id : Id.t = Classes.new_instance_program ~global ~poly name bl t props info in @@ -1057,8 +1057,8 @@ let vernac_instance_program ~atts name bl t props info = let vernac_instance_interactive ~atts name bl t info = Dumpglob.dump_constraint (fst name) false "inst"; - let (program, locality), poly = - Attributes.(parse (Notations.(program ++ locality ++ polymorphic))) atts + let locality, poly = + Attributes.(parse (Notations.(locality ++ polymorphic))) atts in let global = not (make_section_locality locality) in let _id, pstate = @@ -1067,8 +1067,8 @@ let vernac_instance_interactive ~atts name bl t info = let vernac_instance ~atts name bl t props info = Dumpglob.dump_constraint (fst name) false "inst"; - let (program, locality), poly = - Attributes.(parse (Notations.(program ++ locality ++ polymorphic))) atts + let locality, poly = + Attributes.(parse (Notations.(locality ++ polymorphic))) atts in let global = not (make_section_locality locality) in let _id : Id.t = @@ -2094,7 +2094,7 @@ let translate_vernac ~atts v = let open Vernacextend in match v with (* Type classes *) | VernacInstance (name, bl, t, props, info) -> - let { DefAttributes.program } = DefAttributes.parse atts in + let atts, program = Attributes.(parse_with_extra program) atts in if program then VtDefault (fun () -> vernac_instance_program ~atts name bl t props info) else begin match props with |