diff options
| author | Gaëtan Gilbert | 2019-10-30 15:01:53 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-11-13 20:16:13 +0100 |
| commit | dd4a0794821725da238f69f89e8da022e78bf72b (patch) | |
| tree | 1a454749aeaffe07f9c10835912ed595a56cb499 | |
| parent | b9def53df5a69d5d4dbf46bd846281220b4fe1db (diff) | |
don't double parse program attribute for vernacinstance
| -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 |