Deprecating Global.type_of_global_in_context.

Removing a few Global.env in the way.

7 files changed, 17 insertions, 16 deletions

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 614b2181d9..62efc72f1f 100644
--- a/vernac/class.ml
+++ b/vernac/class.ml
@@ -66,7 +66,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))
 
@@ -249,7 +249,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 3cf5e9bfdf..ca0387fd1b 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -70,7 +70,7 @@ let existing_instance glob g info =
   let c = 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 5f2818c12b..8d691eb3b2 100644
--- a/vernac/indschemes.ml
+++ b/vernac/indschemes.ml
@@ -387,7 +387,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 04dcb7d565..23e53ce673 100644
--- a/vernac/search.ml
+++ b/vernac/search.ml
@@ -80,7 +80,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 =