Remove [constr_of_global_in_context] in funind

2 files changed, 11 insertions, 9 deletions

diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 9ca91d62da..60a98c5e6f 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -676,11 +676,15 @@ let build_case_scheme fa =
 (*   in  *)
   let funs =
     let (_,f,_) = fa in
-    try fst (Global.constr_of_global_in_context (Global.env ()) (Smartlocate.global_with_alias f))
+    try (let open GlobRef in
+         match Smartlocate.global_with_alias f with
+         | ConstRef c -> c
+         | IndRef _ | ConstructRef _ | VarRef _ -> assert false)
     with Not_found ->
       user_err ~hdr:"FunInd.build_case_scheme"
         (str "Cannot find " ++ Libnames.pr_qualid f) in
-  let first_fun,u = destConst  funs in
+  let sigma, (_,u) = Evd.fresh_constant_instance env sigma funs in
+  let first_fun = funs in
   let funs_mp = Constant.modpath first_fun in
   let first_fun_kn = try fst (find_Function_infos  first_fun).graph_ind with Not_found -> raise No_graph_found in
   let this_block_funs_indexes = get_funs_constant funs_mp first_fun in
@@ -688,7 +692,7 @@ let build_case_scheme fa =
   let prop_sort = InProp in
   let funs_indexes =
     let this_block_funs_indexes = Array.to_list this_block_funs_indexes in
-    List.assoc_f Constant.equal (fst (destConst funs)) this_block_funs_indexes
+    List.assoc_f Constant.equal funs this_block_funs_indexes
   in
   let (ind, sf) =
 	 let ind = first_fun_kn,funs_indexes in
@@ -718,7 +722,7 @@ let build_case_scheme fa =
       (Some princ_name)
       this_block_funs
       0
-      (prove_princ_for_struct (ref (Evd.from_env (Global.env ()))) false 0 [|fst (destConst funs)|])
+      (prove_princ_for_struct (ref (Evd.from_env (Global.env ()))) false 0 [|funs|])
   in
   ()
  
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 9fa333c629..ca3160f4c4 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -24,6 +24,7 @@ open Globnames
 open Nameops
 open CErrors
 open Util
+open UnivGen
 open Tacticals
 open Tacmach
 open Tactics
@@ -50,7 +51,7 @@ open Context.Rel.Declaration
 (* Ugly things which should not be here *)
 
 [@@@ocaml.warning "-3"]
-let coq_constant m s = EConstr.of_constr @@ UnivGen.constr_of_global @@
+let coq_constant m s = EConstr.of_constr @@ constr_of_global @@
   Coqlib.find_reference "RecursiveDefinition" m s
 
 let arith_Nat = ["Coq"; "Arith";"PeanoNat";"Nat"]
@@ -62,7 +63,7 @@ let pr_leconstr_rd =
 
 let coq_init_constant s =
   EConstr.of_constr (
-    UnivGen.constr_of_global @@
+    constr_of_global @@
     Coqlib.gen_reference_in_modules "RecursiveDefinition" Coqlib.init_modules s)
 [@@@ocaml.warning "+3"]
 
@@ -96,9 +97,6 @@ let type_of_const sigma t =
       Typeops.type_of_constant_in (Global.env()) (sp, u)
     |_ -> assert false
 
-let constr_of_global x = 
-  fst (Global.constr_of_global_in_context (Global.env ()) x)
-
 let constant sl s = constr_of_global (find_reference sl s)
 
 let const_of_ref = function