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.

4 files changed, 15 insertions, 13 deletions

diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index 743d1d2026..5323c9f1c6 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -139,7 +139,7 @@ let build_beq_scheme_deps kn =
        perfomed in a much cleaner way, e.g. using the kernel normal form of
        constructor types and kernel whd_all for the argument types. *)
     let rec aux accu c =
-      let (c,a) = Reductionops.whd_betaiota_stack Evd.empty EConstr.(of_constr c) in
+      let (c,a) = Reductionops.whd_betaiota_stack env Evd.empty EConstr.(of_constr c) in
       let (c,a) = EConstr.Unsafe.(to_constr c, List.map to_constr a) in
       match Constr.kind c with
       | Cast (x,_,_) -> aux accu (Term.applist (x,a))
@@ -238,7 +238,7 @@ let build_beq_scheme mode kn =
     let compute_A_equality rel_list nlist eqA ndx t =
       let lifti = ndx in
       let rec aux c =
-        let (c,a) = Reductionops.whd_betaiota_stack Evd.empty EConstr.(of_constr c) in
+        let (c,a) = Reductionops.whd_betaiota_stack env Evd.empty EConstr.(of_constr c) in
         let (c,a) = EConstr.Unsafe.(to_constr c, List.map to_constr a) in
         match Constr.kind c with
         | Rel x -> mkRel (x-nlist+ndx)
diff --git a/vernac/comCoercion.ml b/vernac/comCoercion.ml
index d6be02245c..3cc5dd65af 100644
--- a/vernac/comCoercion.ml
+++ b/vernac/comCoercion.ml
@@ -111,7 +111,7 @@ la liste des variables dont depend la classe source
 l'indice de la classe source dans la liste lp
 *)
 
-let get_source lp source =
+let get_source env lp source =
   let open Context.Rel.Declaration in
   match source with
     | None ->
@@ -120,7 +120,7 @@ let get_source lp source =
          | [] -> raise Not_found
          | LocalDef _ :: lt -> aux lt
          | LocalAssum (_,t1) :: lt ->
-            let cl1,u1,lv1 = find_class_type Evd.empty (EConstr.of_constr t1) in
+            let cl1,u1,lv1 = find_class_type env Evd.empty (EConstr.of_constr t1) in
             cl1,lt,lv1,1
        in aux lp
     | Some cl ->
@@ -130,17 +130,17 @@ let get_source lp source =
          | LocalDef _ as decl :: lt -> aux (decl::acc) lt
          | LocalAssum (_,t1) as decl :: lt ->
             try
-              let cl1,u1,lv1 = find_class_type Evd.empty (EConstr.of_constr t1) in
+              let cl1,u1,lv1 = find_class_type env Evd.empty (EConstr.of_constr t1) in
               if cl_typ_eq cl cl1 then cl1,acc,lv1,Context.Rel.nhyps lt+1
               else raise Not_found
             with Not_found -> aux (decl::acc) lt
        in aux [] (List.rev lp)
 
-let get_target t ind =
+let get_target env t ind =
   if (ind > 1) then
     CL_FUN
   else
-    match pi1 (find_class_type Evd.empty (EConstr.of_constr t)) with
+    match pi1 (find_class_type env Evd.empty (EConstr.of_constr t)) with
     | CL_CONST p when Recordops.is_primitive_projection p ->
       CL_PROJ (Option.get @@ Recordops.find_primitive_projection p)
     | x -> x
@@ -209,7 +209,7 @@ let build_id_coercion idf_opt source poly =
     match idf_opt with
       | Some idf -> idf
       | None ->
-          let cl,u,_ = find_class_type sigma (EConstr.of_constr t) in
+          let cl,u,_ = find_class_type env sigma (EConstr.of_constr t) in
           Id.of_string ("Id_"^(ident_key_of_class source)^"_"^
                         (ident_key_of_class cl))
   in
@@ -298,14 +298,15 @@ let warn_uniform_inheritance =
 
 let add_new_coercion_core coef stre poly source target isid =
   check_source source;
-  let t, _ = Typeops.type_of_global_in_context (Global.env ()) coef in
+  let env = Global.env () in
+  let t, _ = Typeops.type_of_global_in_context env coef in
   if coercion_exists coef then raise (CoercionError AlreadyExists);
   let lp,tg = decompose_prod_assum t in
   let llp = List.length lp in
   if Int.equal llp 0 then raise (CoercionError NotAFunction);
   let (cls,ctx,lvs,ind) =
     try
-      get_source lp source
+      get_source env lp source
     with Not_found ->
       raise (CoercionError (NoSource source))
   in
@@ -315,7 +316,7 @@ let add_new_coercion_core coef stre poly source target isid =
     warn_uniform_inheritance coef;
   let clt =
     try
-      get_target tg ind
+      get_target env tg ind
     with Not_found ->
       raise (CoercionError NoTarget)
   in
diff --git a/vernac/comHints.ml b/vernac/comHints.ml
index 2fd6fe2b29..ec37ec7fa8 100644
--- a/vernac/comHints.ml
+++ b/vernac/comHints.ml
@@ -33,7 +33,7 @@ let project_hint ~poly pri l2r r =
   let p = if l2r then lib_ref "core.iff.proj1" else lib_ref "core.iff.proj2" in
   let sigma, p = Evd.fresh_global env sigma p in
   let c =
-    Reductionops.whd_beta sigma
+    Reductionops.whd_beta env sigma
       (mkApp (c, Context.Rel.to_extended_vect mkRel 0 sign))
   in
   let c =
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index 3b9c771b93..53f3c8408b 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -1755,7 +1755,8 @@ let cache_scope_command o =
 
 let subst_scope_command (subst,(local,scope,o as x)) = match o with
   | ScopeClasses cl ->
-      let cl' = List.map_filter (subst_scope_class subst) cl in
+      let env = Global.env () in
+      let cl' = List.map_filter (subst_scope_class env subst) cl in
       let cl' =
         if List.for_all2eq (==) cl cl' then cl
         else cl' in