A few Global.env removed.

9 files changed, 36 insertions, 37 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index d52830a16..6dd7022b1 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -50,9 +50,9 @@ let error_bad_pattern_loc loc env sigma cstr ind =
   raise_pattern_matching_error
     (loc, env, sigma, BadPattern (cstr,ind))
 
-let error_bad_constructor_loc loc cstr ind =
+let error_bad_constructor_loc loc env cstr ind =
   raise_pattern_matching_error
-    (loc, Global.env(), Evd.empty, BadConstructor (cstr,ind))
+    (loc, env, Evd.empty, BadConstructor (cstr,ind))
 
 let error_wrong_numarg_constructor_loc loc env c n =
   raise_pattern_matching_error (loc, env, Evd.empty, WrongNumargConstructor(c,n))
@@ -472,14 +472,13 @@ let check_and_adjust_constructor env ind cstrs = function
 	    let args' = adjust_local_defs loc (args, List.rev ci.cs_args)
 	    in PatCstr (loc, cstr, args', alias)
 	  with NotAdjustable ->
-	    error_wrong_numarg_constructor_loc loc (Global.env())
-	      cstr nb_args_constr
+	    error_wrong_numarg_constructor_loc loc env cstr nb_args_constr
       else
 	(* Try to insert a coercion *)
 	try
-	  Coercion.inh_pattern_coerce_to loc pat ind' ind
+	  Coercion.inh_pattern_coerce_to loc env pat ind' ind
 	with Not_found ->
-	  error_bad_constructor_loc loc cstr ind
+	  error_bad_constructor_loc loc env cstr ind
 
 let check_all_variables env sigma typ mat =
   List.iter
@@ -1968,7 +1967,7 @@ let constr_of_pat env evdref arsign pat avoid =
 	    {uj_val = ty; uj_type = Typing.type_of env !evdref ty}
 	in
 	let (ind,u), params = dest_ind_family indf in
-	if not (eq_ind ind cind) then error_bad_constructor_loc l cstr ind;
+	if not (eq_ind ind cind) then error_bad_constructor_loc l env cstr ind;
 	let cstrs = get_constructors env indf in
 	let ci = cstrs.(i-1) in
 	let nb_args_constr = ci.cs_nargs in
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 73534210c..ae1c4eea0 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -295,9 +295,9 @@ let lookup_path_to_fun_from env sigma s =
 let lookup_path_to_sort_from env sigma s =
   apply_on_class_of env sigma s lookup_path_to_sort_from_class
 
-let get_coercion_constructor coe =
+let get_coercion_constructor env coe =
   let c, _ =
-    Reductionops.whd_betadeltaiota_stack (Global.env()) Evd.empty coe.coe_value
+    Reductionops.whd_betadeltaiota_stack env Evd.empty coe.coe_value
   in
   match kind_of_term c with
   | Construct (cstr,u) ->
@@ -305,10 +305,10 @@ let get_coercion_constructor coe =
   | _ ->
       raise Not_found
 
-let lookup_pattern_path_between (s,t) =
+let lookup_pattern_path_between env (s,t) =
   let i = inductive_class_of s in
   let j = inductive_class_of t in
-  List.map get_coercion_constructor (ClPairMap.find (i,j) !inheritance_graph)
+  List.map (get_coercion_constructor env) (ClPairMap.find (i,j) !inheritance_graph)
 
 (* coercion_value : coe_index -> unsafe_judgment * bool *)
 
diff --git a/pretyping/classops.mli b/pretyping/classops.mli
index 1db7bbd61..e423dd247 100644
--- a/pretyping/classops.mli
+++ b/pretyping/classops.mli
@@ -88,7 +88,7 @@ val lookup_path_to_fun_from : env -> evar_map -> types ->
 val lookup_path_to_sort_from : env -> evar_map -> types ->
       types * inheritance_path
 val lookup_pattern_path_between :
-  inductive * inductive -> (constructor * int) list
+  env -> inductive * inductive -> (constructor * int) list
 
 (**/**)
 (* Crade *)
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 0ec25d402..504d73cb8 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -82,8 +82,8 @@ let apply_pattern_coercion loc pat p =
     pat p
 
 (* raise Not_found if no coercion found *)
-let inh_pattern_coerce_to loc pat ind1 ind2 =
-  let p = lookup_pattern_path_between (ind1,ind2) in
+let inh_pattern_coerce_to loc env pat ind1 ind2 =
+  let p = lookup_pattern_path_between env (ind1,ind2) in
     apply_pattern_coercion loc pat p
 
 (* Program coercions *)
diff --git a/pretyping/coercion.mli b/pretyping/coercion.mli
index c1b114c91..1b67b0926 100644
--- a/pretyping/coercion.mli
+++ b/pretyping/coercion.mli
@@ -59,4 +59,4 @@ val inh_conv_coerces_to : Loc.t ->
     pattern [pat] typed in [ind1] into a pattern typed in [ind2];
     raises [Not_found] if no coercion found *)
 val inh_pattern_coerce_to :
-  Loc.t  -> cases_pattern -> inductive -> inductive -> cases_pattern
+  Loc.t -> env -> cases_pattern -> inductive -> inductive -> cases_pattern
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index cebb45266..2f9606b72 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -428,7 +428,7 @@ let cleared = Store.field ()
 
 exception Depends of Id.t
 
-let rec check_and_clear_in_constr evdref err ids c =
+let rec check_and_clear_in_constr env evdref err ids c =
   (* returns a new constr where all the evars have been 'cleaned'
      (ie the hypotheses ids have been removed from the contexts of
      evars) *)
@@ -441,14 +441,14 @@ let rec check_and_clear_in_constr evdref err ids c =
 	  check id'; c
 
       | ( Const _ | Ind _ | Construct _ ) ->
-          let vars = Environ.vars_of_global (Global.env()) c in
+          let vars = Environ.vars_of_global env c in
             Id.Set.iter check vars; c
 
       | Evar (evk,l as ev) ->
 	  if Evd.is_defined !evdref evk then
 	    (* If evk is already defined we replace it by its definition *)
 	    let nc = whd_evar !evdref c in
-	      (check_and_clear_in_constr evdref err ids nc)
+	      (check_and_clear_in_constr env evdref err ids nc)
 	  else
 	    (* We check for dependencies to elements of ids in the
 	       evar_info corresponding to e and in the instance of
@@ -482,7 +482,7 @@ let rec check_and_clear_in_constr evdref err ids c =
 	    let _nconcl =
 	      try
                 let nids = Id.Map.domain rids in
-                check_and_clear_in_constr evdref (EvarTypingBreak ev) nids (evar_concl evi)
+                check_and_clear_in_constr env evdref (EvarTypingBreak ev) nids (evar_concl evi)
 	      with ClearDependencyError (rid,err) ->
 		raise (ClearDependencyError (Id.Map.find rid rids,err)) in
 
@@ -501,19 +501,19 @@ let rec check_and_clear_in_constr evdref err ids c =
 	    (* spiwack: /hacking session *)
               whd_evar !evdref c
 
-      | _ -> map_constr (check_and_clear_in_constr evdref err ids) c
+      | _ -> map_constr (check_and_clear_in_constr env evdref err ids) c
 
-let clear_hyps_in_evi_main evdref hyps terms ids =
+let clear_hyps_in_evi_main env evdref hyps terms ids =
   (* clear_hyps_in_evi erases hypotheses ids in hyps, checking if some
      hypothesis does not depend on a element of ids, and erases ids in
      the contexts of the evars occuring in evi *)
   let terms =
-    List.map (check_and_clear_in_constr evdref (OccurHypInSimpleClause None) ids) terms in
+    List.map (check_and_clear_in_constr env evdref (OccurHypInSimpleClause None) ids) terms in
   let nhyps =
     let check_context ((id,ob,c) as decl) =
       let err = OccurHypInSimpleClause (Some id) in
-      let ob' = Option.smartmap (fun c -> check_and_clear_in_constr evdref err ids c) ob in
-      let c' = check_and_clear_in_constr evdref err ids c in
+      let ob' = Option.smartmap (fun c -> check_and_clear_in_constr env evdref err ids c) ob in
+      let c' = check_and_clear_in_constr env evdref err ids c in
       if ob == ob' && c == c' then decl else (id, ob', c')
     in
     let check_value vk = match force_lazy_val vk with
@@ -531,13 +531,13 @@ let clear_hyps_in_evi_main evdref hyps terms ids =
   in
   (nhyps,terms)
 
-let clear_hyps_in_evi evdref hyps concl ids =
-  match clear_hyps_in_evi_main evdref hyps [concl] ids with
+let clear_hyps_in_evi env evdref hyps concl ids =
+  match clear_hyps_in_evi_main env evdref hyps [concl] ids with
   | (nhyps,[nconcl]) -> (nhyps,nconcl)
   | _ -> assert false
 
-let clear_hyps2_in_evi evdref hyps t concl ids =
-  match clear_hyps_in_evi_main evdref hyps [t;concl] ids with
+let clear_hyps2_in_evi env evdref hyps t concl ids =
+  match clear_hyps_in_evi_main env evdref hyps [t;concl] ids with
   | (nhyps,[t;nconcl]) -> (nhyps,t,nconcl)
   | _ -> assert false
 
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index de55a643a..f38c1ea0f 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -208,10 +208,10 @@ exception ClearDependencyError of Id.t * clear_dependency_error
     used by [Goal] and (indirectly) [Proofview] to handle the clear tactic gracefully*)
 val cleared : bool Store.field
 
-val clear_hyps_in_evi : evar_map ref -> named_context_val -> types ->
+val clear_hyps_in_evi : env -> evar_map ref -> named_context_val -> types ->
   Id.Set.t -> named_context_val * types
 
-val clear_hyps2_in_evi : evar_map ref -> named_context_val -> types -> types ->
+val clear_hyps2_in_evi : env -> evar_map ref -> named_context_val -> types -> types ->
   Id.Set.t -> named_context_val * types * types
 
 val push_rel_context_to_named_context : Environ.env -> types ->
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 008df0096..5de7b901d 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -101,14 +101,14 @@ let check_typability env sigma c =
    (instead of iterating on the list of identifier to be removed, which
    forces the user to give them in order). *)
 
-let clear_hyps sigma ids sign cl =
+let clear_hyps env sigma ids sign cl =
   let evdref = ref (Evd.create_goal_evar_defs sigma) in
-  let (hyps,cl) = Evarutil.clear_hyps_in_evi evdref sign cl ids in
+  let (hyps,cl) = Evarutil.clear_hyps_in_evi env evdref sign cl ids in
   (hyps, cl, !evdref)
 
-let clear_hyps2 sigma ids sign t cl =
+let clear_hyps2 env sigma ids sign t cl =
   let evdref = ref (Evd.create_goal_evar_defs sigma) in
-  let (hyps,t,cl) = Evarutil.clear_hyps2_in_evi evdref sign t cl ids in
+  let (hyps,t,cl) = Evarutil.clear_hyps2_in_evi env evdref sign t cl ids in
   (hyps, t, cl, !evdref)
 
 (* The ClearBody tactic *)
@@ -548,7 +548,7 @@ let prim_refiner r sigma goal =
 	let sign,t,cl,sigma =
 	  if replace then
 	    let nexthyp = get_hyp_after id (named_context_of_val sign) in
-	    let sign,t,cl,sigma = clear_hyps2 sigma (Id.Set.singleton id) sign t cl in
+	    let sign,t,cl,sigma = clear_hyps2 env sigma (Id.Set.singleton id) sign t cl in
 	    move_hyp true false ([],(id,None,t),named_context_of_val sign)
 	      nexthyp,
 	      t,cl,sigma
@@ -672,7 +672,7 @@ let prim_refiner r sigma goal =
     (* And now the structural rules *)
     | Thin ids ->
         let ids = List.fold_left (fun accu x -> Id.Set.add x accu) Id.Set.empty ids in
-	let (hyps,concl,nsigma) = clear_hyps sigma ids sign cl in
+	let (hyps,concl,nsigma) = clear_hyps env sigma ids sign cl in
 	let (gl,ev,sigma) =
 	  Goal.V82.mk_goal nsigma hyps concl (Goal.V82.extra nsigma goal)
 	in
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 2e65aa8d7..365591242 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -1025,4 +1025,4 @@ module NonLogical = Proofview_monad.NonLogical
 let tclLIFT = Proofview_monad.Logical.lift
 
 let tclCHECKINTERRUPT =
-  tclLIFT (NonLogical.make Control.check_for_interrupt)
+   tclLIFT (NonLogical.make Control.check_for_interrupt)