diff options
Diffstat (limited to 'toplevel')
-rw-r--r-- | toplevel/classes.ml | 6 | ||||
-rw-r--r-- | toplevel/command.ml | 14 | ||||
-rw-r--r-- | toplevel/record.ml | 3 | ||||
-rw-r--r-- | toplevel/vernacentries.ml | 2 |
4 files changed, 11 insertions, 14 deletions
diff --git a/toplevel/classes.ml b/toplevel/classes.ml index f63ae3ecb..4a8ce920f 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -230,8 +230,8 @@ let new_class id par ar sup props = (DefinitionEntry proj_entry, IsDefinition Definition) in let cref = ConstRef cst in - Impargs.declare_manual_implicits false cref (Impargs.is_implicit_args()) arity_imps; - Impargs.declare_manual_implicits false (ConstRef proj_cst) (Impargs.is_implicit_args()) (List.hd fieldimpls); + Impargs.declare_manual_implicits false cref arity_imps; + Impargs.declare_manual_implicits false (ConstRef proj_cst) (List.hd fieldimpls); set_rigid cst; cref, [proj_name, Some proj_cst] | _ -> @@ -321,7 +321,7 @@ let fail_on_free_vars = function let instance_hook k pri global imps ?hook cst = let inst = Typeclasses.new_instance k pri global cst in - Impargs.maybe_declare_manual_implicits false (ConstRef cst) false imps; + Impargs.maybe_declare_manual_implicits false (ConstRef cst) ~enriching:false imps; Typeclasses.add_instance inst; (match hook with Some h -> h cst | None -> ()) diff --git a/toplevel/command.ml b/toplevel/command.ml index 9ae3f8e82..c8acd8113 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -136,7 +136,7 @@ let red_constant_entry bl ce = function let declare_global_definition ident ce local imps = let kn = declare_constant ident (DefinitionEntry ce,IsDefinition Definition) in let gr = ConstRef kn in - maybe_declare_manual_implicits false gr (is_implicit_args ()) imps; + maybe_declare_manual_implicits false gr imps; if local = Local && Flags.is_verbose() then msg_warning (pr_id ident ++ str" is declared as a global definition"); definition_message ident; @@ -189,7 +189,7 @@ let declare_one_assumption is_coe (local,kind) c imps impl keep nl (_,ident) = let kn = declare_constant ident (ParameterEntry (c,nl), IsAssumption kind) in let gr = ConstRef kn in - maybe_declare_manual_implicits false gr (is_implicit_args ()) imps; + maybe_declare_manual_implicits false gr imps; assumption_message ident; if local=Local & Flags.is_verbose () then msg_warning (pr_id ident ++ str" is declared as a parameter" ++ @@ -625,12 +625,10 @@ let declare_mutual_with_eliminations isrecord mie impls = let (_,kn) = declare_mind isrecord mie in list_iter_i (fun i (indimpls, constrimpls) -> let ind = (kn,i) in - maybe_declare_manual_implicits false (IndRef ind) - (is_implicit_args()) indimpls; + maybe_declare_manual_implicits false (IndRef ind) indimpls; list_iter_i (fun j impls -> - maybe_declare_manual_implicits false (ConstructRef (ind, succ j)) - (is_implicit_args()) impls) + maybe_declare_manual_implicits false (ConstructRef (ind, succ j)) impls) constrimpls) impls; if_verbose ppnl (minductive_message names); @@ -785,7 +783,7 @@ let declare_fix boxed kind f def t imps = } in let kn = declare_constant f (DefinitionEntry ce,IsDefinition kind) in let gr = ConstRef kn in - maybe_declare_manual_implicits false gr (is_implicit_args ()) imps; + maybe_declare_manual_implicits false gr imps; gr let prepare_recursive_declaration fixnames fixtypes fixdefs = @@ -1209,7 +1207,7 @@ let start_proof_com kind thms hook = list_map_i (save_remaining_recthms kind body opaq) 1 other_thms in let thms_data = (strength,ref,imps)::other_thms_data in List.iter (fun (strength,ref,imps) -> - maybe_declare_manual_implicits false ref (is_implicit_args ()) imps; + maybe_declare_manual_implicits false ref imps; hook strength ref) thms_data in start_proof id kind t ?init_tac:rec_tac hook diff --git a/toplevel/record.ml b/toplevel/record.ml index ae97a8db4..8ac103fba 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -198,8 +198,7 @@ let declare_projections indsp ?(kind=StructureComponent) ?name coers fieldimpls raise (NotDefinable (BadTypedProj (fid,ctx,te))) in let refi = ConstRef kn in let constr_fi = mkConst kn in - Impargs.maybe_declare_manual_implicits - false refi (Impargs.is_implicit_args()) impls; + Impargs.maybe_declare_manual_implicits false refi impls; if coe then begin let cl = Class.class_of_global (IndRef indsp) in Class.try_add_new_coercion_with_source refi Global cl diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 399c18c92..8f2d3c1e3 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -751,7 +751,7 @@ let vernac_syntactic_definition lid = let vernac_declare_implicits local r = function | Some imps -> - Impargs.declare_manual_implicits local (global_with_alias r) false + Impargs.declare_manual_implicits local (global_with_alias r) ~enriching:false (List.map (fun (ex,b,f) -> ex, (b,f)) imps) | None -> Impargs.declare_implicits local (global_with_alias r) |