Merge PR #8687: Mini reorganization type of global constr of global

21 files changed, 105 insertions, 88 deletions

diff --git a/engine/univGen.mli b/engine/univGen.mli
index 42756701dc..8af5f8fdb0 100644
--- a/engine/univGen.mli
+++ b/engine/univGen.mli
@@ -89,3 +89,4 @@ val constr_of_global : GlobRef.t -> constr
     references and computing their instantiated universe context. (side-effect on the
     universe counter, use with care). *)
 val type_of_global : GlobRef.t -> types in_universe_context_set
+[@@ocaml.deprecated "use [Typeops.type_of_global]"]
diff --git a/interp/impargs.ml b/interp/impargs.ml
index ce33cb8731..d8582d856e 100644
--- a/interp/impargs.ml
+++ b/interp/impargs.ml
@@ -450,13 +450,13 @@ let compute_mib_implicits flags kn =
       (Array.mapi  (* No need to lift, arities contain no de Bruijn *)
         (fun i mip ->
 	  (** No need to care about constraints here *)
-	  let ty, _ = Global.type_of_global_in_context env (IndRef (kn,i)) in
+          let ty, _ = Typeops.type_of_global_in_context env (IndRef (kn,i)) in
 	  Context.Rel.Declaration.LocalAssum (Name mip.mind_typename, ty))
         mib.mind_packets) in
   let env_ar = Environ.push_rel_context ar env in
   let imps_one_inductive i mip =
     let ind = (kn,i) in
-    let ar, _ = Global.type_of_global_in_context env (IndRef ind) in
+    let ar, _ = Typeops.type_of_global_in_context env (IndRef ind) in
     ((IndRef ind,compute_semi_auto_implicits env sigma flags (of_constr ar)),
      Array.mapi (fun j c ->
        (ConstructRef (ind,j+1),compute_semi_auto_implicits env_ar sigma flags c))
@@ -694,7 +694,7 @@ let declare_manual_implicits local ref ?enriching l =
   let flags = !implicit_args in
   let env = Global.env () in
   let sigma = Evd.from_env env in
-  let t, _ = Global.type_of_global_in_context env ref in
+  let t, _ = Typeops.type_of_global_in_context env ref in
   let t = of_constr t in
   let enriching = Option.default flags.auto enriching in
   let autoimpls = compute_auto_implicits env sigma flags enriching t in
diff --git a/interp/notation.ml b/interp/notation.ml
index 6104ab16c7..db8ee5bc18 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -1314,7 +1314,7 @@ let rebuild_arguments_scope sigma (req,r,n,l,_) =
     | ArgsScopeNoDischarge -> assert false
     | ArgsScopeAuto ->
       let env = Global.env () in (*FIXME?*)
-      let typ = EConstr.of_constr @@ fst (Global.type_of_global_in_context env r) in
+      let typ = EConstr.of_constr @@ fst (Typeops.type_of_global_in_context env r) in
       let scs,cls = compute_arguments_scope_full sigma typ in
       (req,r,List.length scs,scs,cls)
     | ArgsScopeManual ->
@@ -1322,7 +1322,7 @@ let rebuild_arguments_scope sigma (req,r,n,l,_) =
          for the extra parameters of the section. Discard the classes
          of the manually given scopes to avoid further re-computations. *)
       let env = Global.env () in (*FIXME?*)
-      let typ = EConstr.of_constr @@ fst (Global.type_of_global_in_context env r) in
+      let typ = EConstr.of_constr @@ fst (Typeops.type_of_global_in_context env r) in
       let l',cls = compute_arguments_scope_full sigma typ in
       let l1 = List.firstn n l' in
       let cls1 = List.firstn n cls in
@@ -1369,7 +1369,7 @@ let find_arguments_scope r =
 
 let declare_ref_arguments_scope sigma ref =
   let env = Global.env () in (* FIXME? *)
-  let typ = EConstr.of_constr @@ fst @@ Global.type_of_global_in_context env ref in
+  let typ = EConstr.of_constr @@ fst @@ Typeops.type_of_global_in_context env ref in
   let (scs,cls as o) = compute_arguments_scope_full sigma typ in
   declare_arguments_scope_gen ArgsScopeAuto ref (List.length scs) o
 
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 164a47dd9a..3481d3bedb 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -319,6 +319,52 @@ let check_fixpoint env lna lar vdef vdeft =
   with NotConvertibleVect i ->
     error_ill_typed_rec_body env i lna (make_judgev vdef vdeft) lar
 
+(* Global references *)
+
+let type_of_global_in_context env r =
+  let open Names.GlobRef in
+  match r with
+  | VarRef id -> Environ.named_type id env, Univ.AUContext.empty
+  | ConstRef c ->
+    let cb = Environ.lookup_constant c env in
+    let univs = Declareops.constant_polymorphic_context cb in
+    cb.Declarations.const_type, univs
+  | IndRef ind ->
+    let (mib,_ as specif) = Inductive.lookup_mind_specif env ind in
+    let univs = Declareops.inductive_polymorphic_context mib in
+    let inst = Univ.make_abstract_instance univs in
+    let env = Environ.push_context ~strict:false (Univ.AUContext.repr univs) env in
+    Inductive.type_of_inductive env (specif, inst), univs
+  | ConstructRef cstr ->
+    let (mib,_ as specif) =
+      Inductive.lookup_mind_specif env (inductive_of_constructor cstr)
+    in
+    let univs = Declareops.inductive_polymorphic_context mib in
+    let inst = Univ.make_abstract_instance univs in
+    Inductive.type_of_constructor (cstr,inst) specif, univs
+
+(* Build a fresh instance for a given context, its associated substitution and
+   the instantiated constraints. *)
+
+let constr_of_global_in_context env r =
+  let open GlobRef in
+  match r with
+  | VarRef id -> mkVar id, Univ.AUContext.empty
+  | ConstRef c ->
+    let cb = lookup_constant c env in
+    let univs = Declareops.constant_polymorphic_context cb in
+    mkConstU (c, Univ.make_abstract_instance univs), univs
+  | IndRef ind ->
+    let (mib,_) = Inductive.lookup_mind_specif env ind in
+    let univs = Declareops.inductive_polymorphic_context mib in
+    mkIndU (ind, Univ.make_abstract_instance univs), univs
+  | ConstructRef cstr ->
+    let (mib,_) =
+      Inductive.lookup_mind_specif env (inductive_of_constructor cstr)
+    in
+    let univs = Declareops.inductive_polymorphic_context mib in
+    mkConstructU (cstr, Univ.make_abstract_instance univs), univs
+
 (************************************************************************)
 (************************************************************************)
 
diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index 57acdfe4b5..1fd070d9d5 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -54,11 +54,10 @@ val type_of_variable : env -> variable -> types
 val judge_of_variable : env -> variable -> unsafe_judgment
 
 (** {6 type of a constant } *)
-
+val type_of_constant_in : env -> pconstant -> types
 val judge_of_constant : env -> pconstant -> unsafe_judgment
 
 (** {6 type of an applied projection } *)
-
 val judge_of_projection : env -> Projection.t -> unsafe_judgment -> unsafe_judgment
 
 (** {6 Type of application. } *)
@@ -89,9 +88,7 @@ val judge_of_cast :
   unsafe_judgment
 
 (** {6 Inductive types. } *)
-
 val judge_of_inductive : env -> inductive puniverses -> unsafe_judgment
-
 val judge_of_constructor : env -> constructor puniverses -> unsafe_judgment
 
 (** {6 Type of Cases. } *)
@@ -99,7 +96,25 @@ val judge_of_case : env -> case_info
   -> unsafe_judgment -> unsafe_judgment -> unsafe_judgment array
     -> unsafe_judgment
 
-val type_of_constant_in : env -> pconstant -> types
+(** {6 Type of global references. } *)
+
+val type_of_global_in_context : env -> GlobRef.t -> types * Univ.AUContext.t
+(** Returns the type of the global reference, by creating a fresh
+    instance of polymorphic references and computing their
+    instantiated universe context. The type should not be used
+    without pushing it's universe context in the environmnent of
+    usage. For non-universe-polymorphic constants, it does not
+    matter. *)
+
+(** {6 Building a term from a global reference *)
+
+(** Map a global reference to a term in its local universe
+    context. The term should not be used without pushing it's universe
+    context in the environmnent of usage. For non-universe-polymorphic
+    constants, it does not matter. *)
+val constr_of_global_in_context : env -> GlobRef.t -> types * Univ.AUContext.t
+
+(** {6 Miscellaneous. } *)
 
 (** Check that hyps are included in env and fails with error otherwise *)
 val check_hyps_inclusion : env -> ('a -> constr) -> 'a -> Constr.named_context -> unit
diff --git a/library/global.ml b/library/global.ml
index 1ad72afea1..3781ff3230 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -167,48 +167,8 @@ let env_of_context hyps =
 
 open Globnames
 
-(** Build a fresh instance for a given context, its associated substitution and 
-    the instantiated constraints. *)
-
-let constr_of_global_in_context env r =
-  let open Constr in
-  match r with
-  | VarRef id -> mkVar id, Univ.AUContext.empty
-  | ConstRef c ->
-    let cb = Environ.lookup_constant c env in
-    let univs = Declareops.constant_polymorphic_context cb in
-    mkConstU (c, Univ.make_abstract_instance univs), univs
-  | IndRef ind ->
-    let (mib, oib as specif) = Inductive.lookup_mind_specif env ind in
-    let univs = Declareops.inductive_polymorphic_context mib in
-    mkIndU (ind, Univ.make_abstract_instance univs), univs
-  | ConstructRef cstr ->
-    let (mib,oib as specif) =
-      Inductive.lookup_mind_specif env (inductive_of_constructor cstr)
-    in
-    let univs = Declareops.inductive_polymorphic_context mib in
-    mkConstructU (cstr, Univ.make_abstract_instance univs), univs
-
-let type_of_global_in_context env r = 
-  match r with
-  | VarRef id -> Environ.named_type id env, Univ.AUContext.empty
-  | ConstRef c -> 
-    let cb = Environ.lookup_constant c env in 
-    let univs = Declareops.constant_polymorphic_context cb in
-    cb.Declarations.const_type, univs
-  | IndRef ind ->
-    let (mib, oib as specif) = Inductive.lookup_mind_specif env ind in
-    let univs = Declareops.inductive_polymorphic_context mib in
-    let inst = Univ.make_abstract_instance univs in
-    let env = Environ.push_context ~strict:false (Univ.AUContext.repr univs) env in
-    Inductive.type_of_inductive env (specif, inst), univs
-  | ConstructRef cstr ->
-    let (mib,oib as specif) =
-      Inductive.lookup_mind_specif env (inductive_of_constructor cstr) 
-    in
-    let univs = Declareops.inductive_polymorphic_context mib in
-    let inst = Univ.make_abstract_instance univs in
-    Inductive.type_of_constructor (cstr,inst) specif, univs
+let constr_of_global_in_context = Typeops.constr_of_global_in_context
+let type_of_global_in_context = Typeops.type_of_global_in_context
 
 let universes_of_global gr = 
   universes_of_global (env ()) gr
diff --git a/library/global.mli b/library/global.mli
index 29255a70ff..42a8005a4f 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -129,17 +129,11 @@ val is_type_in_type : GlobRef.t -> bool
 
 val constr_of_global_in_context : Environ.env ->
   GlobRef.t -> Constr.types * Univ.AUContext.t
-(** Returns the type of the constant in its local universe
-    context. The type should not be used without pushing it's universe
-    context in the environmnent of usage. For non-universe-polymorphic
-    constants, it does not matter. *)
+  [@@ocaml.deprecated "alias of [Typeops.constr_of_global_in_context]"]
 
 val type_of_global_in_context : Environ.env -> 
   GlobRef.t -> Constr.types * Univ.AUContext.t
-(** Returns the type of the constant in its local universe
-    context. The type should not be used without pushing it's universe
-    context in the environmnent of usage. For non-universe-polymorphic
-    constants, it does not matter. *)
+  [@@ocaml.deprecated "alias of [Typeops.type_of_global]"]
 
 (** Returns the universe context of the global reference (whatever its polymorphic status is). *)
 val universes_of_global : GlobRef.t -> Univ.AUContext.t
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index 7b4fd280bd..f6eea3c5c4 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -446,7 +446,7 @@ let error_MPfile_as_mod mp b =
 
 let argnames_of_global r =
   let env = Global.env () in
-  let typ, _ = Global.type_of_global_in_context env r in
+  let typ, _ = Typeops.type_of_global_in_context env r in
   let rels,_ =
     decompose_prod (Reduction.whd_all env typ) in
   List.rev_map fst rels
@@ -878,7 +878,7 @@ let extract_constant_inline inline r ids s =
   match g with
     | ConstRef kn ->
 	let env = Global.env () in
-	let typ, _ = Global.type_of_global_in_context env (ConstRef kn) in
+        let typ, _ = Typeops.type_of_global_in_context env (ConstRef kn) in
 	let typ = Reduction.whd_all env typ in
 	if Reduction.is_arity env typ
 	  then begin
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index a385a61ae0..28a9542167 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -311,7 +311,7 @@ let pr_info f_info =
   str "function_constant_type := " ++
   (try
      Printer.pr_lconstr_env env sigma
-       (fst (Global.type_of_global_in_context env (ConstRef f_info.function_constant)))
+       (fst (Typeops.type_of_global_in_context env (ConstRef f_info.function_constant)))
    with e when CErrors.noncritical e -> mt ()) ++ fnl () ++
   str "equation_lemma := " ++ pr_ocst f_info.equation_lemma ++ fnl () ++
   str "completeness_lemma :=" ++ pr_ocst f_info.completeness_lemma ++ fnl () ++
diff --git a/plugins/ssr/ssrvernac.mlg b/plugins/ssr/ssrvernac.mlg
index 876751911b..940defb743 100644
--- a/plugins/ssr/ssrvernac.mlg
+++ b/plugins/ssr/ssrvernac.mlg
@@ -360,7 +360,7 @@ let coerce_search_pattern_to_sort hpat =
     Pattern.PApp (fp, args') in
   let hr, na = splay_search_pattern 0 hpat in
   let dc, ht =
-    let hr, _ = Global.type_of_global_in_context (Global.env ()) hr (** FIXME *) in
+    let hr, _ = Typeops.type_of_global_in_context env hr (** FIXME *) in
     Reductionops.splay_prod env sigma (EConstr.of_constr hr) in
   let np = List.length dc in
   if np < na then CErrors.user_err (Pp.str "too many arguments in head search pattern") else
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 73141191cf..2c2a8fe49e 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -379,7 +379,7 @@ type coercion = {
 (* Computation of the class arity *)
 
 let reference_arity_length ref =
-  let t, _ = Global.type_of_global_in_context (Global.env ()) ref in
+  let t, _ = Typeops.type_of_global_in_context (Global.env ()) ref in
   List.length (fst (Reductionops.splay_arity (Global.env()) Evd.empty (EConstr.of_constr t))) (** FIXME *)
 
 let projection_arity_length p =
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index ce12aaeeb0..0bc35e5358 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -279,7 +279,7 @@ let build_subclasses ~check env sigma glob { hint_priority = pri } =
       (fun () -> incr i;
         Nameops.add_suffix _id ("_subinstance_" ^ string_of_int !i))
   in
-  let ty, ctx = Global.type_of_global_in_context env glob in
+  let ty, ctx = Typeops.type_of_global_in_context env glob in
   let inst, ctx = UnivGen.fresh_instance_from ctx None in
   let ty = Vars.subst_instance_constr inst ty in
   let ty = EConstr.of_constr ty in
@@ -420,7 +420,7 @@ let remove_instance i =
   remove_instance_hint i.is_impl
 
 let declare_instance info local glob =
-  let ty, _ = Global.type_of_global_in_context (Global.env ()) glob in
+  let ty, _ = Typeops.type_of_global_in_context (Global.env ()) glob in
   let info = Option.default {hint_priority = None; hint_pattern = None} info in
     match class_of_constr Evd.empty (EConstr.of_constr ty) with
     | Some (rels, ((tc,_), args) as _cl) ->
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index e6f82c60ee..4619e049e0 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -71,7 +71,7 @@ let int_or_no n = if Int.equal n 0 then str "no" else int n
 let print_basename sp = pr_global (ConstRef sp)
 
 let print_ref reduce ref udecl =
-  let typ, univs = Global.type_of_global_in_context (Global.env ()) ref in
+  let typ, univs = Typeops.type_of_global_in_context (Global.env ()) ref in
   let inst = Univ.make_abstract_instance univs in
   let bl = UnivNames.universe_binders_with_opt_names ref udecl in
   let sigma = Evd.from_ctx (UState.of_binders bl) in
@@ -147,7 +147,7 @@ let print_renames_list prefix l =
     hv 2 (prlist_with_sep pr_comma (fun x -> x) (List.map Name.print l))]
 
 let need_expansion impl ref =
-  let typ, _ = Global.type_of_global_in_context (Global.env ()) ref in
+  let typ, _ = Typeops.type_of_global_in_context (Global.env ()) ref in
   let ctx = Term.prod_assum typ in
   let nprods = List.count is_local_assum ctx in
   not (List.is_empty impl) && List.length impl >= nprods &&
@@ -823,7 +823,7 @@ let print_opaque_name env sigma qid =
     | IndRef (sp,_) ->
         print_inductive sp None
     | ConstructRef cstr as gr ->
-	let ty, ctx = Global.type_of_global_in_context env gr in
+        let ty, ctx = Typeops.type_of_global_in_context env gr in
 	let ty = EConstr.of_constr ty in
         let open EConstr in
         print_typed_value_in_env env sigma (mkConstruct cstr, ty)
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 0c10f32c86..2f2d32e887 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -942,7 +942,7 @@ let make_extern pri pat tacast =
 
 let make_mode ref m = 
   let open Term in
-  let ty, _ = Global.type_of_global_in_context (Global.env ()) ref in
+  let ty, _ = Typeops.type_of_global_in_context (Global.env ()) ref in
   let ctx, t = decompose_prod ty in
   let n = List.length ctx in
   let m' = Array.of_list m in
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index 9f71def8fc..fa1b8eeb3e 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -113,7 +113,7 @@ let mkFullInd (ind,u) n =
     else mkIndU (ind,u)
 
 let check_bool_is_defined () =
-  try let _ = Global.type_of_global_in_context (Global.env ()) Coqlib.(lib_ref "core.bool.type") in ()
+  try let _ = Typeops.type_of_global_in_context (Global.env ()) Coqlib.(lib_ref "core.bool.type") in ()
   with e when CErrors.noncritical e -> raise (UndefinedCst "bool")
 
 let check_no_indices mib =
diff --git a/vernac/class.ml b/vernac/class.ml
index 526acd40b5..ab43d5c8ff 100644
--- a/vernac/class.ml
+++ b/vernac/class.ml
@@ -65,7 +65,7 @@ let explain_coercion_error g = function
 
 let check_reference_arity ref =
   let env = Global.env () in
-  let c, _ = Global.type_of_global_in_context env ref in
+  let c, _ = Typeops.type_of_global_in_context env ref in
   if not (Reductionops.is_arity env (Evd.from_env env) (EConstr.of_constr c)) (** FIXME *) then
     raise (CoercionError (NotAClass ref))
 
@@ -248,7 +248,7 @@ let warn_uniform_inheritance =
 
 let add_new_coercion_core coef stre poly source target isid =
   check_source source;
-  let t, _ = Global.type_of_global_in_context (Global.env ()) coef in
+  let t, _ = Typeops.type_of_global_in_context (Global.env ()) coef in
   if coercion_exists coef then raise (CoercionError AlreadyExists);
   let lp,tg = decompose_prod_assum t in
   let llp = List.length lp in
diff --git a/vernac/classes.ml b/vernac/classes.ml
index 52c1e1cf98..84ffb84206 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -69,7 +69,7 @@ let existing_instance glob g info =
   let c = Nametab.global g in
   let info = Option.default Hints.empty_hint_info info in
   let info = intern_info info in
-  let instance, _ = Global.type_of_global_in_context (Global.env ()) c in
+  let instance, _ = Typeops.type_of_global_in_context (Global.env ()) c in
   let _, r = Term.decompose_prod_assum instance in
     match class_of_constr Evd.empty (EConstr.of_constr r) with
       | Some (_, ((tc,u), _)) -> add_instance (new_instance tc info glob c)
diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml
index 4efbb968fb..d8cd429e6e 100644
--- a/vernac/indschemes.ml
+++ b/vernac/indschemes.ml
@@ -386,7 +386,7 @@ let do_mutual_induction_scheme ?(force_mutual=false) lnamedepindsort =
        let evd, indu, inst =
 	 match inst with
 	 | None ->
-	    let _, ctx = Global.type_of_global_in_context env0 (IndRef ind) in
+            let _, ctx = Typeops.type_of_global_in_context env0 (IndRef ind) in
             let u, ctx = UnivGen.fresh_instance_from ctx None in
             let evd = Evd.from_ctx (UState.of_context_set ctx) in
 	      evd, (ind,u), Some u
diff --git a/vernac/record.ml b/vernac/record.ml
index 724b6e62fe..3ba360fee4 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -574,8 +574,8 @@ let declare_class finite def cum ubinders univs id idbuild paramimpls params ari
   List.map map data
 
 
-let add_constant_class cst =
-  let ty, univs = Global.type_of_global_in_context (Global.env ()) (ConstRef cst) in
+let add_constant_class env cst =
+  let ty, univs = Typeops.type_of_global_in_context env (ConstRef cst) in
   let ctx, arity = decompose_prod_assum ty in
   let tc = 
     { cl_univs = univs;
@@ -589,12 +589,12 @@ let add_constant_class cst =
   in add_class tc;
     set_typeclass_transparency (EvalConstRef cst) false false
       
-let add_inductive_class ind =
-  let mind, oneind = Global.lookup_inductive ind in
+let add_inductive_class env ind =
+  let mind, oneind = Inductive.lookup_mind_specif env ind in
   let k =
     let ctx = oneind.mind_arity_ctxt in
     let univs = Declareops.inductive_polymorphic_context mind in
-    let env = push_context ~strict:false (Univ.AUContext.repr univs) (Global.env ()) in
+    let env = push_context ~strict:false (Univ.AUContext.repr univs) env in
     let env = push_rel_context ctx env in
     let inst = Univ.make_abstract_instance univs in
     let ty = Inductive.type_of_inductive env ((mind, oneind), inst) in
@@ -612,11 +612,12 @@ let warn_already_existing_class =
       Printer.pr_global g ++ str " is already declared as a typeclass.")
 
 let declare_existing_class g =
+  let env = Global.env () in
   if Typeclasses.is_class g then warn_already_existing_class g
   else
     match g with
-    | ConstRef x -> add_constant_class x
-    | IndRef x -> add_inductive_class x
+    | ConstRef x -> add_constant_class env x
+    | IndRef x -> add_inductive_class env x
     | _ -> user_err ~hdr:"declare_existing_class"
              (Pp.str"Unsupported class type, only constants and inductives are allowed")
 
diff --git a/vernac/search.ml b/vernac/search.ml
index 2273130668..1fac28358a 100644
--- a/vernac/search.ml
+++ b/vernac/search.ml
@@ -79,7 +79,7 @@ let iter_declarations (fn : GlobRef.t -> env -> constr -> unit) =
   | "CONSTANT" ->
     let cst = Global.constant_of_delta_kn kn in
     let gr = ConstRef cst in
-    let (typ, _) = Global.type_of_global_in_context (Global.env ()) gr in
+    let (typ, _) = Typeops.type_of_global_in_context (Global.env ()) gr in
       fn gr env typ
   | "INDUCTIVE" ->
     let mind = Global.mind_of_delta_kn kn in
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 48d4165830..1190d73258 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1101,6 +1101,8 @@ let warn_arguments_assert =
    [args] is the main list of arguments statuses,
    [more_implicits] is a list of extra lists of implicit statuses  *)
 let vernac_arguments ~atts reference args more_implicits nargs_for_red flags =
+  let env = Global.env () in
+  let sigma = Evd.from_env env in
   let assert_flag = List.mem `Assert flags in
   let rename_flag = List.mem `Rename flags in
   let clear_scopes_flag = List.mem `ClearScopes flags in
@@ -1125,9 +1127,7 @@ let vernac_arguments ~atts reference args more_implicits nargs_for_red flags =
 
   let sr = smart_global reference in
   let inf_names =
-    let ty, _ = Global.type_of_global_in_context (Global.env ()) sr in
-    let env = Global.env () in
-    let sigma = Evd.from_env env in
+    let ty, _ = Typeops.type_of_global_in_context env sr in
     Impargs.compute_implicits_names env sigma (EConstr.of_constr ty)
   in
   let prev_names =