Deprecating Global.type_of_global_in_context.

Removing a few Global.env in the way.

2 files changed, 6 insertions, 6 deletions

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