No more local reduction functions in Reductionops.

This is extracted from #9710, where we need the environment anyway to compute
iota rules on inductive types with let-bindings. The commit is self-contained,
so I think it could go directly in to save me a few rebases.

Furthermore, this is also related to #11707. Assuming we split cbn from the
other reduction machine, this allows to merge the "local" machine with
the general one, since after this PR they will have the same type. One less
reduction machine should make people happy.

6 files changed, 25 insertions, 23 deletions

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