Remove references to Global.env in tactics/*.ml

Only in ml files that are not related to Coq commands

1 files changed, 18 insertions, 22 deletions

diff --git a/tactics/equality.ml b/tactics/equality.ml
index 66345ce43..d08735582 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -334,25 +334,27 @@ let (forward_general_setoid_rewrite_clause, general_setoid_rewrite_clause) = Hoo
 
 (* Do we have a JMeq instance on twice the same domains ? *)
 
-let jmeq_same_dom gl = function
+let jmeq_same_dom env sigma = function
   | None -> true (* already checked in Hipattern.find_eq_data_decompose *)
   | Some t ->
-    let rels, t = decompose_prod_assum (project gl) t in
-    let env = push_rel_context rels (Proofview.Goal.env gl) in
-    match decompose_app (project gl) t with
-      | _, [dom1; _; dom2;_] -> is_conv env (Tacmach.New.project gl) dom1 dom2
+    let rels, t = decompose_prod_assum sigma t in
+    let env = push_rel_context rels env in
+    match decompose_app sigma t with
+      | _, [dom1; _; dom2;_] -> is_conv env sigma dom1 dom2
       | _ -> false
 
 (* find_elim determines which elimination principle is necessary to
    eliminate lbeq on sort_of_gl. *)
 
-let find_elim hdcncl lft2rgt dep cls ot gl =
+let find_elim hdcncl lft2rgt dep cls ot =
+  Proofview.Goal.enter_one begin fun gl ->
   let sigma = project gl in
   let is_global gr c = Termops.is_global sigma gr c in
   let inccl = Option.is_empty cls in
+  let env = Proofview.Goal.env gl in
   if (is_global Coqlib.glob_eq hdcncl ||
       (is_global Coqlib.glob_jmeq hdcncl &&
-	 jmeq_same_dom gl ot)) && not dep
+	 jmeq_same_dom env sigma ot)) && not dep
   then
     let c = 
       match EConstr.kind sigma hdcncl with 
@@ -382,9 +384,7 @@ let find_elim hdcncl lft2rgt dep cls ot gl =
 	     Logic.eq or Jmeq just before *)
 	assert false
     in
-      let (sigma, elim) = fresh_global (Global.env ()) (Proofview.Goal.sigma gl) (ConstRef c) in
-      let elim = EConstr.of_constr elim in
-      (sigma, (elim, Safe_typing.empty_private_constants))
+        pf_constr_of_global (ConstRef c) 
   else
   let scheme_name = match dep, lft2rgt, inccl with
     (* Non dependent case *)
@@ -400,14 +400,12 @@ let find_elim hdcncl lft2rgt dep cls ot gl =
   in
   match EConstr.kind sigma hdcncl with
   | Ind (ind,u) -> 
+      
       let c, eff = find_scheme scheme_name ind in 
-      (* MS: cannot use pf_constr_of_global as the eliminator might be generated by side-effect *)
-      let (sigma, elim) =
-	fresh_global (Global.env ()) (Proofview.Goal.sigma gl) (ConstRef c)
-      in
-      let elim = EConstr.of_constr elim in
-      (sigma, (elim, eff))
+      Proofview.tclEFFECTS eff <*>
+        pf_constr_of_global (ConstRef c) 
   | _ -> assert false
+  end
 
 let type_of_clause cls gl = match cls with
   | None -> Proofview.Goal.concl gl
@@ -420,9 +418,7 @@ let leibniz_rewrite_ebindings_clause cls lft2rgt tac c t l with_evars frzevars d
   let dep_fun = if isatomic then dependent else dependent_no_evar in
   let type_of_cls = type_of_clause cls gl in
   let dep = dep_proof_ok && dep_fun evd c type_of_cls in
-  let (sigma, (elim, effs)) = find_elim hdcncl lft2rgt dep cls (Some t) gl in
-      Proofview.Unsafe.tclEVARS sigma <*>
-      Proofview.tclEFFECTS effs <*>
+  find_elim hdcncl lft2rgt dep cls (Some t) >>= fun elim ->
       general_elim_clause with_evars frzevars tac cls c t l
       (match lft2rgt with None -> false | Some b -> b)
       {elimindex = None; elimbody = (elim,NoBindings); elimrename = None}
@@ -536,7 +532,7 @@ let general_rewrite_clause l2r with_evars ?tac c cl =
 	let do_hyps =
 	  (* If the term to rewrite uses an hypothesis H, don't rewrite in H *)
 	  let ids gl =
-	    let ids_in_c = Termops.global_vars_set (Global.env()) (project gl) (fst c) in
+	    let ids_in_c = Termops.global_vars_set (Proofview.Goal.env gl) (project gl) (fst c) in
             let ids_of_hyps = pf_ids_of_hyps gl in
 	    Id.Set.fold (fun id l -> List.remove Id.equal id l) ids_in_c ids_of_hyps
 	  in
@@ -988,7 +984,7 @@ let discrimination_pf env sigma e (t,t1,t2) discriminator lbeq =
   let sigma, i           = build_coq_I sigma in
   let sigma, absurd_term = build_coq_False sigma in
   let eq_elim, eff       = ind_scheme_of_eq lbeq in
-  let sigma, eq_elim = Evd.fresh_global (Global.env ()) sigma eq_elim in
+  let sigma, eq_elim = Evd.fresh_global env sigma eq_elim in
   let eq_elim = EConstr.of_constr eq_elim in
     sigma, (applist (eq_elim, [t;t1;mkNamedLambda e t discriminator;i;t2]), absurd_term),
     eff
@@ -1536,7 +1532,7 @@ let decomp_tuple_term env sigma c t =
   let rec decomprec inner_code ex exty =
     let iterated_decomp =
     try
-      let ({proj1=p1; proj2=p2}),(i,a,p,car,cdr) = find_sigma_data_decompose sigma ex in
+      let ({proj1=p1; proj2=p2}),(i,a,p,car,cdr) = find_sigma_data_decompose env sigma ex in
       let car_code = applist (mkConstU (destConstRef p1,i),[a;p;inner_code])
       and cdr_code = applist (mkConstU (destConstRef p2,i),[a;p;inner_code]) in
       let cdrtyp = beta_applist sigma (p,[car]) in