Merge PR #11922: No more local reduction functions in Reductionops.

Reviewed-by: Matafou
Ack-by: SkySkimmer
Reviewed-by: gares

12 files changed, 37 insertions, 34 deletions

diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index afc83b780b..0f96b9bbe8 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -259,7 +259,7 @@ let parse_ind_args si args relmax =
 
 
 let rec extract_type env sg db j c args =
-  match EConstr.kind sg (whd_betaiotazeta sg c) with
+  match EConstr.kind sg (whd_betaiotazeta env sg c) with
     | App (d, args') ->
         (* We just accumulate the arguments. *)
         extract_type env sg db j d (Array.to_list args' @ args)
@@ -380,7 +380,7 @@ and extract_type_app env sg db (r,s) args =
 and extract_type_scheme env sg db c p =
   if Int.equal p 0 then extract_type env sg db 0 c []
   else
-    let c = whd_betaiotazeta sg c in
+    let c = whd_betaiotazeta env sg c in
     match EConstr.kind sg c with
       | Lambda (n,t,d) ->
           extract_type_scheme (push_rel_assum (n,t) env) sg db d (p-1)
diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index 834e4251d3..f13901c36d 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -57,12 +57,12 @@ let make_simple_atoms seq=
       | None->[]
   in {negative=seq.latoms;positive=ratoms}
 
-let do_sequent sigma setref triv id seq i dom atoms=
+let do_sequent env sigma setref triv id seq i dom atoms=
   let flag=ref true in
   let phref=ref triv in
   let do_atoms a1 a2 =
     let do_pair t1 t2 =
-      match unif_atoms sigma i dom t1 t2 with
+      match unif_atoms env sigma i dom t1 t2 with
           None->()
         | Some (Phantom _) ->phref:=true
         | Some c ->flag:=false;setref:=IS.add (c,id) !setref in
@@ -72,16 +72,16 @@ let do_sequent sigma setref triv id seq i dom atoms=
     do_atoms atoms (make_simple_atoms seq);
     !flag && !phref
 
-let match_one_quantified_hyp sigma setref seq lf=
+let match_one_quantified_hyp env sigma setref seq lf=
   match lf.pat with
       Left(Lforall(i,dom,triv))|Right(Rexists(i,dom,triv))->
-        if do_sequent sigma setref triv lf.id seq i dom lf.atoms then
+        if do_sequent env sigma setref triv lf.id seq i dom lf.atoms then
           setref:=IS.add ((Phantom dom),lf.id) !setref
     | _ -> anomaly (Pp.str "can't happen.")
 
-let give_instances sigma lf seq=
+let give_instances env sigma lf seq=
   let setref=ref IS.empty in
-    List.iter (match_one_quantified_hyp sigma setref seq) lf;
+    List.iter (match_one_quantified_hyp env sigma setref seq) lf;
     IS.elements !setref
 
 (* collector for the engine *)
@@ -129,9 +129,10 @@ let left_instance_tac (inst,id) continue seq=
   let open EConstr in
   Proofview.Goal.enter begin fun gl ->
   let sigma = project gl in
+  let env = Proofview.Goal.env gl in
   match inst with
       Phantom dom->
-        if lookup sigma (id,None) seq then
+        if lookup env sigma (id,None) seq then
           tclFAIL 0 (Pp.str "already done")
         else
           tclTHENS (cut dom)
@@ -148,7 +149,7 @@ let left_instance_tac (inst,id) continue seq=
             tclTRY assumption]
     | Real((m,t),_)->
         let c = (m, EConstr.to_constr sigma t) in
-        if lookup sigma (id,Some c) seq then
+        if lookup env sigma (id,Some c) seq then
           tclFAIL 0 (Pp.str "already done")
         else
           let special_generalize=
@@ -205,7 +206,8 @@ let instance_tac inst=
 
 let quantified_tac lf backtrack continue seq =
   Proofview.Goal.enter begin fun gl ->
-  let insts=give_instances (project gl) lf seq in
+  let env = Proofview.Goal.env gl in
+  let insts=give_instances env (project gl) lf seq in
     tclORELSE
       (tclFIRST (List.map (fun inst->instance_tac inst continue seq) insts))
       backtrack
diff --git a/plugins/firstorder/instances.mli b/plugins/firstorder/instances.mli
index c0f4c78ff3..08c2c4d916 100644
--- a/plugins/firstorder/instances.mli
+++ b/plugins/firstorder/instances.mli
@@ -13,7 +13,7 @@ open Rules
 
 val collect_quantified : Evd.evar_map -> Sequent.t -> Formula.t list * Sequent.t
 
-val give_instances : Evd.evar_map -> Formula.t list -> Sequent.t ->
+val give_instances : Environ.env -> Evd.evar_map -> Formula.t list -> Sequent.t ->
   (Unify.instance * GlobRef.t) list
 
 val quantified_tac : Formula.t list -> seqtac with_backtracking
diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml
index 7bf13fd25b..3dd5059e5d 100644
--- a/plugins/firstorder/sequent.ml
+++ b/plugins/firstorder/sequent.ml
@@ -109,7 +109,7 @@ let deepen seq={seq with depth=seq.depth-1}
 
 let record item seq={seq with history=History.add item seq.history}
 
-let lookup sigma item seq=
+let lookup env sigma item seq=
   History.mem item seq.history ||
   match item with
       (_,None)->false
@@ -117,7 +117,7 @@ let lookup sigma item seq=
         let p (id2,o)=
           match o with
               None -> false
-            | Some (m2, t2)-> GlobRef.equal id id2 && m2>m && more_general sigma (m2, EConstr.of_constr t2) (m, EConstr.of_constr t) in
+            | Some (m2, t2)-> GlobRef.equal id id2 && m2>m && more_general env sigma (m2, EConstr.of_constr t2) (m, EConstr.of_constr t) in
           History.exists p seq.history
 
 let add_formula env sigma side nam t seq =
diff --git a/plugins/firstorder/sequent.mli b/plugins/firstorder/sequent.mli
index 3a5da6ad14..bba89c823c 100644
--- a/plugins/firstorder/sequent.mli
+++ b/plugins/firstorder/sequent.mli
@@ -39,7 +39,7 @@ val deepen: t -> t
 
 val record: h_item -> t -> t
 
-val lookup: Evd.evar_map -> h_item -> t -> bool
+val lookup: Environ.env -> Evd.evar_map -> h_item -> t -> bool
 
 val add_formula : Environ.env -> Evd.evar_map -> side -> GlobRef.t -> constr -> t -> t
 
diff --git a/plugins/firstorder/unify.ml b/plugins/firstorder/unify.ml
index e58e80116d..9c3debe48f 100644
--- a/plugins/firstorder/unify.ml
+++ b/plugins/firstorder/unify.ml
@@ -29,7 +29,7 @@ let subst_meta subst t =
   let subst = List.map (fun (m, c) -> (m, EConstr.Unsafe.to_constr c)) subst in
   EConstr.of_constr (subst_meta subst (EConstr.Unsafe.to_constr t))
 
-let unif evd t1 t2=
+let unif env evd t1 t2=
   let bige=Queue.create ()
   and sigma=ref [] in
   let bind i t=
@@ -46,8 +46,8 @@ let unif evd t1 t2=
     Queue.add (t1,t2) bige;
     try while true do
       let t1,t2=Queue.take bige in
-      let nt1=head_reduce (whd_betaiotazeta evd t1)
-      and nt2=head_reduce (whd_betaiotazeta evd t2) in
+      let nt1=head_reduce (whd_betaiotazeta env evd t1)
+      and nt2=head_reduce (whd_betaiotazeta env evd t2) in
         match (EConstr.kind evd nt1),(EConstr.kind evd nt2) with
             Meta i,Meta j->
               if not (Int.equal i j) then
@@ -123,9 +123,9 @@ let mk_rel_inst evd t=
   in
   let nt=renum_rec 0 t in (!new_rel - 1,nt)
 
-let unif_atoms evd i dom t1 t2=
+let unif_atoms env evd i dom t1 t2=
   try
-    let t=Int.List.assoc i (unif evd t1 t2) in
+    let t=Int.List.assoc i (unif env evd t1 t2) in
       if isMeta evd t then Some (Phantom dom)
       else Some (Real(mk_rel_inst evd t,value evd i t1))
   with
@@ -136,11 +136,11 @@ let renum_metas_from k n t= (* requires n = max (free_rels t) *)
   let l=List.init n (fun i->mkMeta (k+i)) in
     substl l t
 
-let more_general evd (m1,t1) (m2,t2)=
+let more_general env evd (m1,t1) (m2,t2)=
   let mt1=renum_metas_from 0 m1 t1
   and mt2=renum_metas_from m1 m2 t2 in
     try
-      let sigma=unif evd mt1 mt2 in
+      let sigma=unif env evd mt1 mt2 in
       let p (n,t)= n<m1 || isMeta evd t in
         List.for_all p sigma
     with UFAIL(_,_)->false
diff --git a/plugins/firstorder/unify.mli b/plugins/firstorder/unify.mli
index 71e786eb90..c6767f04ac 100644
--- a/plugins/firstorder/unify.mli
+++ b/plugins/firstorder/unify.mli
@@ -13,12 +13,12 @@ open EConstr
 
 exception UFAIL of constr*constr
 
-val unif : Evd.evar_map -> constr -> constr -> (int*constr) list
+val unif : Environ.env -> Evd.evar_map -> constr -> constr -> (int*constr) list
 
 type instance=
     Real of (int*constr)*int (* nb trous*terme*valeur heuristique *)
   | Phantom of constr        (* domaine de quantification *)
 
-val unif_atoms : Evd.evar_map -> metavariable -> constr -> constr -> constr -> instance option
+val unif_atoms : Environ.env -> Evd.evar_map -> metavariable -> constr -> constr -> constr -> instance option
 
-val more_general : Evd.evar_map -> (int*constr) -> (int*constr) -> bool
+val more_general : Environ.env -> Evd.evar_map -> (int*constr) -> (int*constr) -> bool
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 49fc513dd2..b864b18887 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -116,7 +116,7 @@ let prove_trivial_eq h_id context (constructor, type_of_term, term) =
         refine to_refine g) ]
 
 let find_rectype env sigma c =
-  let t, l = decompose_app sigma (Reductionops.whd_betaiotazeta sigma c) in
+  let t, l = decompose_app sigma (Reductionops.whd_betaiotazeta env sigma c) in
   match EConstr.kind sigma t with
   | Ind ind -> (t, l)
   | Construct _ -> (t, l)
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 3b8fb48eb0..d6b2a17882 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -478,7 +478,7 @@ let error_no_relation () = user_err Pp.(str "Cannot find a relation to rewrite."
 
 let rec decompose_app_rel env evd t =
   (* Head normalize for compatibility with the old meta mechanism *)
-  let t = Reductionops.whd_betaiota evd t in
+  let t = Reductionops.whd_betaiota env evd t in
   match EConstr.kind evd t with
   | App (f, [||]) -> assert false
   | App (f, [|arg|]) ->
@@ -711,7 +711,7 @@ let unify_eqn (car, rel, prf, c1, c2, holes, sort) l2r flags env (sigma, cstrs)
     let sigma = Typeclasses.resolve_typeclasses ~filter:(no_constraints cstrs)
       ~fail:true env sigma in
     let evd = solve_remaining_by env sigma holes by in
-    let nf c = Reductionops.nf_evar evd (Reductionops.nf_meta evd c) in
+    let nf c = Reductionops.nf_evar evd (Reductionops.nf_meta env evd c) in
     let c1 = nf c1 and c2 = nf c2
     and rew_car = nf car and rel = nf rel
     and prf = nf prf in
@@ -971,7 +971,7 @@ let unfold_match env sigma sk app =
   | App (f', args) when Constant.equal (fst (destConst sigma f')) sk ->
       let v = Environ.constant_value_in (Global.env ()) (sk,Univ.Instance.empty)(*FIXME*) in
       let v = EConstr.of_constr v in
-        Reductionops.whd_beta sigma (mkApp (v, args))
+        Reductionops.whd_beta env sigma (mkApp (v, args))
   | _ -> app
 
 let is_rew_cast = function RewCast _ -> true | _ -> false
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index e8257b5dba..01e8daf82d 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -950,7 +950,7 @@ let saturate ?(beta=false) ?(bi_types=false) env sigma c ?(ty=Retyping.get_type_
   let open EConstr in
   if n = 0 then
     let args = List.rev args in
-     (if beta then Reductionops.whd_beta sigma else fun x -> x)
+     (if beta then Reductionops.whd_beta env sigma else fun x -> x)
       (EConstr.mkApp (c, Array.of_list (List.map snd args))), ty, args, sigma
   else match kind_of_type sigma ty with
   | ProdType (_, src, tgt) ->
@@ -1065,11 +1065,12 @@ end
 let introid ?(orig=ref Anonymous) name =
   let open Proofview.Notations in
   Proofview.Goal.enter begin fun gl ->
+    let env = Proofview.Goal.env gl in
     let sigma = Proofview.Goal.sigma gl in
     let g = Proofview.Goal.concl gl in
    match EConstr.kind sigma g with
    | App (hd, _) when EConstr.isLambda sigma hd ->
-      convert_concl_no_check (Reductionops.whd_beta sigma g)
+      convert_concl_no_check (Reductionops.whd_beta env sigma g)
    | _ -> Tacticals.New.tclIDTAC
   end <*>
     (fst_prod false (fun id -> orig := id; Tactics.intro_mustbe_force name))
diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml
index ab07dd5be9..29a9c65561 100644
--- a/plugins/ssr/ssrequality.ml
+++ b/plugins/ssr/ssrequality.ml
@@ -281,7 +281,7 @@ let unfoldintac occ rdx t (kt,_) =
           | App (f,a) when EConstr.eq_constr sigma0 f t -> EConstr.mkApp (body env f f,a)
           | Proj _ when same_proj sigma0 c t -> body env t c
           | _ ->
-            let c = Reductionops.whd_betaiotazeta sigma0 c in
+            let c = Reductionops.whd_betaiotazeta env sigma0 c in
             match EConstr.kind sigma0 c with
             | Const _ when EConstr.eq_constr sigma0 c t -> body env t t
             | App (f,a) when EConstr.eq_constr sigma0 f t -> EConstr.mkApp (body env f f,a)
@@ -516,7 +516,7 @@ let rwprocess_rule env dir rule =
     let rec loop d sigma r t0 rs red =
       let t =
         if red = 1 then Tacred.hnf_constr env sigma t0
-        else Reductionops.whd_betaiotazeta sigma t0 in
+        else Reductionops.whd_betaiotazeta env sigma t0 in
       ppdebug(lazy Pp.(str"rewrule="++pr_econstr_pat env sigma t));
       match EConstr.kind sigma t with
       | Prod (_, xt, at) ->
diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml
index adaf7c8cc1..e004613ef3 100644
--- a/plugins/ssrmatching/ssrmatching.ml
+++ b/plugins/ssrmatching/ssrmatching.ml
@@ -405,7 +405,7 @@ let evars_for_FO ~hack env sigma0 (ise0:evar_map) c0 =
 (* p_origin can be passed to obtain a better error message     *)
 let mk_tpattern ?p_origin ?(hack=false) env sigma0 (ise, t) ok dir p =
   let k, f, a =
-    let f, a = Reductionops.whd_betaiota_stack ise (EConstr.of_constr p) in
+    let f, a = Reductionops.whd_betaiota_stack env ise (EConstr.of_constr p) in
     let f = EConstr.Unsafe.to_constr f in
     let a = List.map EConstr.Unsafe.to_constr a in
     match kind f with