From 2826683746569b9d78aa01e319315ab554e1619b Mon Sep 17 00:00:00 2001 From: Gaetan Gilbert Date: Fri, 21 Apr 2017 19:36:45 +0200 Subject: Fix omitted labels in function calls --- vernac/class.ml | 4 ++-- vernac/command.ml | 4 ++-- vernac/ind_tables.ml | 6 +++--- vernac/metasyntax.ml | 2 +- 4 files changed, 8 insertions(+), 8 deletions(-) (limited to 'vernac') diff --git a/vernac/class.ml b/vernac/class.ml index 95114ec39..104f3c1db 100644 --- a/vernac/class.ml +++ b/vernac/class.ml @@ -311,7 +311,7 @@ let add_coercion_hook poly local ref = | Global -> false | Discharge -> assert false in - let () = try_add_new_coercion ref stre poly in + let () = try_add_new_coercion ref ~local:stre poly in let msg = pr_global_env Id.Set.empty ref ++ str " is now a coercion" in Flags.if_verbose Feedback.msg_info msg @@ -324,6 +324,6 @@ let add_subclass_hook poly local ref = | Discharge -> assert false in let cl = class_of_global ref in - try_add_new_coercion_subclass cl stre poly + try_add_new_coercion_subclass cl ~local:stre poly let add_subclass_hook poly = Lemmas.mk_hook (add_subclass_hook poly) diff --git a/vernac/command.ml b/vernac/command.ml index b27d8a0a3..b2f5755ce 100644 --- a/vernac/command.ml +++ b/vernac/command.ml @@ -258,7 +258,7 @@ match local with let () = Universes.register_universe_binders gr pl in let () = assumption_message ident in let () = Typeclasses.declare_instance None false gr in - let () = if is_coe then Class.try_add_new_coercion gr local p in + let () = if is_coe then Class.try_add_new_coercion gr ~local p in let inst = if p (* polymorphic *) then Univ.UContext.instance ctx else Univ.Instance.empty @@ -752,7 +752,7 @@ let do_mutual_inductive indl poly prv finite = (* Declare the possible notations of inductive types *) List.iter Metasyntax.add_notation_interpretation ntns; (* Declare the coercions *) - List.iter (fun qid -> Class.try_add_new_coercion (locate qid) false poly) coes; + List.iter (fun qid -> Class.try_add_new_coercion (locate qid) ~local:false poly) coes; (* If positivity is assumed declares itself as unsafe. *) if Environ.deactivated_guard (Global.env ()) then Feedback.feedback Feedback.AddedAxiom else () diff --git a/vernac/ind_tables.ml b/vernac/ind_tables.ml index 85d0b6194..c6588684a 100644 --- a/vernac/ind_tables.ml +++ b/vernac/ind_tables.ml @@ -151,7 +151,7 @@ let define_individual_scheme_base kind suff f mode idopt (mind,i as ind) = let const = define mode id c mib.mind_polymorphic ctx in declare_scheme kind [|ind,const|]; const, Safe_typing.add_private - (Safe_typing.private_con_of_scheme kind (Global.safe_env()) [ind,const]) eff + (Safe_typing.private_con_of_scheme ~kind (Global.safe_env()) [ind,const]) eff let define_individual_scheme kind mode names (mind,i as ind) = match Hashtbl.find scheme_object_table kind with @@ -172,7 +172,7 @@ let define_mutual_scheme_base kind suff f mode names mind = consts, Safe_typing.add_private (Safe_typing.private_con_of_scheme - kind (Global.safe_env()) (Array.to_list schemes)) + ~kind (Global.safe_env()) (Array.to_list schemes)) eff let define_mutual_scheme kind mode names mind = @@ -185,7 +185,7 @@ let find_scheme_on_env_too kind ind = let s = String.Map.find kind (Indmap.find ind !scheme_map) in s, Safe_typing.add_private (Safe_typing.private_con_of_scheme - kind (Global.safe_env()) [ind, s]) + ~kind (Global.safe_env()) [ind, s]) Safe_typing.empty_private_constants let find_scheme ?(mode=InternalTacticRequest) kind (mind,i as ind) = diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index f805eeaa9..f86a0ef92 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -1196,7 +1196,7 @@ let inNotation : notation_obj -> obj = (**********************************************************************) let with_lib_stk_protection f x = - let fs = Lib.freeze `No in + let fs = Lib.freeze ~marshallable:`No in try let a = f x in Lib.unfreeze fs; a with reraise -> let reraise = CErrors.push reraise in -- cgit v1.2.3