diff options
Diffstat (limited to 'vernac/ind_tables.ml')
| -rw-r--r-- | vernac/ind_tables.ml | 6 |
1 files changed, 3 insertions, 3 deletions
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) = |