diff options
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/command.ml | 2 | ||||
| -rw-r--r-- | toplevel/search.ml | 4 |
2 files changed, 3 insertions, 3 deletions
diff --git a/toplevel/command.ml b/toplevel/command.ml index 90376a4311..e85c4299b7 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -332,7 +332,7 @@ let extract_mutual_inductive_declaration_components indl = let declare_mutual_inductive_with_eliminations isrecord mie impls = let names = List.map (fun e -> e.mind_entry_typename) mie.mind_entry_inds in let (_,kn) = declare_mind isrecord mie in - let mind = Global.mind_of_delta (mind_of_kn kn) in + let mind = Global.mind_of_delta_kn kn in list_iter_i (fun i (indimpls, constrimpls) -> let ind = (mind,i) in Autoinstance.search_declaration (IndRef ind); diff --git a/toplevel/search.ml b/toplevel/search.ml index 7b5d770d27..33e8e51dba 100644 --- a/toplevel/search.ml +++ b/toplevel/search.ml @@ -65,14 +65,14 @@ let gen_crible refopt (fn : global_reference -> env -> constr -> unit) = fn (VarRef id) env typ with Not_found -> (* we are in a section *) ()) | "CONSTANT" -> - let cst = Global.constant_of_delta(constant_of_kn kn) in + let cst = Global.constant_of_delta_kn kn in let typ = Typeops.type_of_constant env cst in if refopt = None || head_const typ = constr_of_global (Option.get refopt) then fn (ConstRef cst) env typ | "INDUCTIVE" -> - let mind = Global.mind_of_delta(mind_of_kn kn) in + let mind = Global.mind_of_delta_kn kn in let mib = Global.lookup_mind mind in (match refopt with | Some (IndRef ((kn',tyi) as ind)) when eq_mind mind kn' -> |