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.

3 files changed, 28 insertions, 26 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index f82783f47d..a1aac60b35 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -187,7 +187,7 @@ let empty_internalization_env = Id.Map.empty
 
 let compute_internalization_data env sigma id ty typ impl =
   let impl = compute_implicits_with_manual env sigma typ (is_implicit_args()) impl in
-  (ty, impl, compute_arguments_scope sigma typ, var_uid id)
+  (ty, impl, compute_arguments_scope env sigma typ, var_uid id)
 
 let compute_internalization_env env sigma ?(impls=empty_internalization_env) ty =
   List.fold_left3
@@ -2358,9 +2358,9 @@ let extract_ids env =
     (Termops.ids_of_rel_context (Environ.rel_context env))
     Id.Set.empty
 
-let scope_of_type_kind sigma = function
+let scope_of_type_kind env sigma = function
   | IsType -> Notation.current_type_scope_name ()
-  | OfType typ -> compute_type_scope sigma typ
+  | OfType typ -> compute_type_scope env sigma typ
   | WithoutTypeConstraint | UnknownIfTermOrType -> None
 
 let allowed_binder_kind_of_type_kind = function
@@ -2377,7 +2377,7 @@ let empty_ltac_sign = {
 let intern_gen kind env sigma
                ?(impls=empty_internalization_env) ?(pattern_mode=false) ?(ltacvars=empty_ltac_sign)
                c =
-  let tmp_scope = scope_of_type_kind sigma kind in
+  let tmp_scope = scope_of_type_kind env sigma kind in
   let k = allowed_binder_kind_of_type_kind kind in
   internalize env {ids = extract_ids env; unb = false;
                          tmp_scope = tmp_scope; scopes = [];
@@ -2462,7 +2462,7 @@ let intern_constr_pattern env sigma ?(as_type=false) ?(ltacvars=empty_ltac_sign)
 
 let intern_core kind env sigma ?(pattern_mode=false) ?(ltacvars=empty_ltac_sign)
       { Genintern.intern_ids = ids; Genintern.notation_variable_status = vl } c =
-  let tmp_scope = scope_of_type_kind sigma kind in
+  let tmp_scope = scope_of_type_kind env sigma kind in
   let impls = empty_internalization_env in
   let k = allowed_binder_kind_of_type_kind kind in
   internalize env
diff --git a/interp/notation.ml b/interp/notation.ml
index 7761606f11..2703930705 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -1448,8 +1448,8 @@ type scope_class = cl_typ
 let scope_class_compare : scope_class -> scope_class -> int =
   cl_typ_ord
 
-let compute_scope_class sigma t =
-  let (cl,_,_) = find_class_type sigma t in
+let compute_scope_class env sigma t =
+  let (cl,_,_) = find_class_type env sigma t in
   cl
 
 module ScopeClassOrd =
@@ -1478,22 +1478,23 @@ let find_scope_class_opt = function
 (**********************************************************************)
 (* Special scopes associated to arguments of a global reference *)
 
-let rec compute_arguments_classes sigma t =
-  match EConstr.kind sigma (Reductionops.whd_betaiotazeta sigma t) with
-    | Prod (_,t,u) ->
-        let cl = try Some (compute_scope_class sigma t) with Not_found -> None in
-        cl :: compute_arguments_classes sigma u
+let rec compute_arguments_classes env sigma t =
+  match EConstr.kind sigma (Reductionops.whd_betaiotazeta env sigma t) with
+    | Prod (na, t, u) ->
+        let env = EConstr.push_rel (Context.Rel.Declaration.LocalAssum (na, t)) env in
+        let cl = try Some (compute_scope_class env sigma t) with Not_found -> None in
+        cl :: compute_arguments_classes env sigma u
     | _ -> []
 
-let compute_arguments_scope_full sigma t =
-  let cls = compute_arguments_classes sigma t in
+let compute_arguments_scope_full env sigma t =
+  let cls = compute_arguments_classes env sigma t in
   let scs = List.map find_scope_class_opt cls in
   scs, cls
 
-let compute_arguments_scope sigma t = fst (compute_arguments_scope_full sigma t)
+let compute_arguments_scope env sigma t = fst (compute_arguments_scope_full env sigma t)
 
-let compute_type_scope sigma t =
-  find_scope_class_opt (try Some (compute_scope_class sigma t) with Not_found -> None)
+let compute_type_scope env sigma t =
+  find_scope_class_opt (try Some (compute_scope_class env sigma t) with Not_found -> None)
 
 let current_type_scope_name () =
    find_scope_class_opt (Some CL_SORT)
@@ -1531,15 +1532,16 @@ let load_arguments_scope _ (_,(_,r,n,scl,cls)) =
 let cache_arguments_scope o =
   load_arguments_scope 1 o
 
-let subst_scope_class subst cs =
-  try Some (subst_cl_typ subst cs) with Not_found -> None
+let subst_scope_class env subst cs =
+  try Some (subst_cl_typ env subst cs) with Not_found -> None
 
 let subst_arguments_scope (subst,(req,r,n,scl,cls)) =
   let r' = fst (subst_global subst r) in
   let subst_cl ocl = match ocl with
     | None -> ocl
     | Some cl ->
-        match subst_scope_class subst cl with
+        let env = Global.env () in
+        match subst_scope_class env subst cl with
         | Some cl'  as ocl' when cl' != cl -> ocl'
         | _ -> ocl in
   let cls' = List.Smart.map subst_cl cls in
@@ -1565,7 +1567,7 @@ let rebuild_arguments_scope sigma (req,r,n,l,_) =
     | ArgsScopeAuto ->
       let env = Global.env () in (*FIXME?*)
       let typ = EConstr.of_constr @@ fst (Typeops.type_of_global_in_context env r) in
-      let scs,cls = compute_arguments_scope_full sigma typ in
+      let scs,cls = compute_arguments_scope_full env sigma typ in
       (req,r,List.length scs,scs,cls)
     | ArgsScopeManual ->
       (* Add to the manually given scopes the one found automatically
@@ -1573,7 +1575,7 @@ let rebuild_arguments_scope sigma (req,r,n,l,_) =
          of the manually given scopes to avoid further re-computations. *)
       let env = Global.env () in (*FIXME?*)
       let typ = EConstr.of_constr @@ fst (Typeops.type_of_global_in_context env r) in
-      let l',cls = compute_arguments_scope_full sigma typ in
+      let l',cls = compute_arguments_scope_full env sigma typ in
       let l1 = List.firstn n l' in
       let cls1 = List.firstn n cls in
       (req,r,0,l1@l,cls1)
@@ -1620,7 +1622,7 @@ let find_arguments_scope r =
 let declare_ref_arguments_scope sigma ref =
   let env = Global.env () in (* FIXME? *)
   let typ = EConstr.of_constr @@ fst @@ Typeops.type_of_global_in_context env ref in
-  let (scs,cls as o) = compute_arguments_scope_full sigma typ in
+  let (scs,cls as o) = compute_arguments_scope_full env sigma typ in
   declare_arguments_scope_gen ArgsScopeAuto ref (List.length scs) o
 
 (********************************)
diff --git a/interp/notation.mli b/interp/notation.mli
index 842f2b1458..b427aa9bb3 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -264,13 +264,13 @@ type scope_class
 val scope_class_compare : scope_class -> scope_class -> int
 
 val subst_scope_class :
-  Mod_subst.substitution -> scope_class -> scope_class option
+  Environ.env -> Mod_subst.substitution -> scope_class -> scope_class option
 
 val declare_scope_class : scope_name -> scope_class -> unit
 val declare_ref_arguments_scope : Evd.evar_map -> GlobRef.t -> unit
 
-val compute_arguments_scope : Evd.evar_map -> EConstr.types -> scope_name option list
-val compute_type_scope : Evd.evar_map -> EConstr.types -> scope_name option
+val compute_arguments_scope : Environ.env -> Evd.evar_map -> EConstr.types -> scope_name option list
+val compute_type_scope : Environ.env -> Evd.evar_map -> EConstr.types -> scope_name option
 
 (** Get the current scope bound to Sortclass, if it exists *)
 val current_type_scope_name : unit -> scope_name option