Merge PR #8864: Avoid passing empty environments

20 files changed, 41 insertions, 68 deletions

diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index ad1114b733..d4e410bd69 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -229,10 +229,6 @@ let isAppConstruct ?(env=Global.env ()) sigma t =
     true
   with Not_found -> false
 
-let nf_betaiotazeta = (* Reductionops.local_strong Reductionops.whd_betaiotazeta  *)
-  Reductionops.clos_norm_flags CClosure.betaiotazeta  Environ.empty_env @@ Evd.from_env Environ.empty_env
-
-
 exception NoChange
 
 let change_eq env sigma hyp_id (context:rel_context) x t end_of_type  =
@@ -420,7 +416,7 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma =
   let rec scan_type  context type_of_hyp : tactic =
     if isLetIn sigma type_of_hyp then
       let real_type_of_hyp = it_mkProd_or_LetIn type_of_hyp context in
-      let reduced_type_of_hyp = nf_betaiotazeta real_type_of_hyp in
+      let reduced_type_of_hyp = Reductionops.nf_betaiotazeta env sigma real_type_of_hyp in
       (* length of context didn't change ? *)
       let new_context,new_typ_of_hyp =
 	 decompose_prod_n_assum sigma (List.length context) reduced_type_of_hyp
@@ -800,7 +796,7 @@ let build_proof
 			g
 		  | LetIn _ ->
 		      let new_infos =
-			{ dyn_infos with info = nf_betaiotazeta dyn_infos.info }
+                        { dyn_infos with info = Reductionops.nf_betaiotazeta env sigma dyn_infos.info }
 		      in
 
 		      tclTHENLIST
@@ -834,7 +830,7 @@ let build_proof
 	  | LetIn _ ->
 	      let new_infos =
 		{ dyn_infos with
-		    info = nf_betaiotazeta dyn_infos.info
+                    info = Reductionops.nf_betaiotazeta env sigma dyn_infos.info
 		}
 	      in
 
@@ -977,7 +973,7 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num
 (*   observe (str "body " ++ pr_lconstr bodies.(num)); *)
   let f_body_with_params_and_other_fun  = substl fnames_with_params bodies.(num) in
 (*   observe (str "f_body_with_params_and_other_fun " ++  pr_lconstr f_body_with_params_and_other_fun); *)
-  let eq_rhs = nf_betaiotazeta (mkApp(compose_lam params f_body_with_params_and_other_fun,Array.init (nb_params + nb_args) (fun i -> mkRel(nb_params + nb_args - i)))) in
+  let eq_rhs = Reductionops.nf_betaiotazeta (Global.env ()) evd (mkApp(compose_lam params f_body_with_params_and_other_fun,Array.init (nb_params + nb_args) (fun i -> mkRel(nb_params + nb_args - i)))) in
   (*   observe (str "eq_rhs " ++  pr_lconstr eq_rhs); *)
   let (type_ctxt,type_of_f),evd =
     let evd,t = Typing.type_of ~refresh:true (Global.env ()) evd f
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index b0842c3721..96eb7fbc60 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -63,12 +63,6 @@ let observe_tac s tac g =
   then do_observe_tac (str s) tac g
   else tac g
 
-(* [nf_zeta] $\zeta$-normalization of a term *)
-let nf_zeta =
-  Reductionops.clos_norm_flags  (CClosure.RedFlags.mkflags [CClosure.RedFlags.fZETA])
-    Environ.empty_env
-    (Evd.from_env Environ.empty_env)
-
 let thin ids gl = Proofview.V82.of_tactic (Tactics.clear ids) gl
 
 (* (\* [id_to_constr id] finds the term associated to [id] in the global environment *\) *)
@@ -219,7 +213,7 @@ let prove_fun_correct evd funs_constr graphs_constr schemes lemmas_types_infos i
     let mib,_ = Global.lookup_inductive graph_ind in
     (* and the principle to use in this lemma in $\zeta$ normal form *)
     let f_principle,princ_type = schemes.(i) in
-    let princ_type =  nf_zeta princ_type in
+    let princ_type = Reductionops.nf_zeta (Global.env ()) evd princ_type in
     let princ_infos = Tactics.compute_elim_sig evd princ_type in
     (* The number of args of the function is then easily computable *)
     let nb_fun_args = nb_prod (project g) (pf_concl g) - 2 in
@@ -397,7 +391,7 @@ let prove_fun_correct evd funs_constr graphs_constr schemes lemmas_types_infos i
 	List.rev (fst  (List.fold_left2
 	  (fun (bindings,avoid) decl p ->
 	     let id = Namegen.next_ident_away (Nameops.Name.get_id (RelDecl.get_name decl)) (Id.Set.of_list avoid) in
-	     (nf_zeta p)::bindings,id::avoid)
+             (Reductionops.nf_zeta (pf_env g) (project g) p)::bindings,id::avoid)
 	  ([],avoid)
 	  princ_infos.predicates
 	  (lemmas)))
@@ -630,12 +624,12 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : Tacmach.tacti
     *)
     let lemmas =
       Array.map
-	(fun (_,(ctxt,concl)) -> nf_zeta (EConstr.it_mkLambda_or_LetIn concl ctxt))
+        (fun (_,(ctxt,concl)) -> Reductionops.nf_zeta (pf_env g) (project g) (EConstr.it_mkLambda_or_LetIn concl ctxt))
 	lemmas_types_infos
     in
     (* We get the constant and the principle corresponding to this lemma *)
     let f = funcs.(i) in
-    let graph_principle = nf_zeta (EConstr.of_constr schemes.(i))  in
+    let graph_principle = Reductionops.nf_zeta (pf_env g) (project g) (EConstr.of_constr schemes.(i))  in
     let princ_type = pf_unsafe_type_of g graph_principle in
     let princ_infos = Tactics.compute_elim_sig (project g) princ_type in
     (* Then we get the number of argument of the function
@@ -771,7 +765,7 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list
 	 let type_of_lemma = EConstr.it_mkProd_or_LetIn type_of_lemma_concl type_of_lemma_ctxt in
          let sigma, _ = Typing.type_of (Global.env ()) !evd type_of_lemma in
          evd := sigma;
-	   let type_of_lemma = nf_zeta type_of_lemma in
+           let type_of_lemma = Reductionops.nf_zeta (Global.env ()) !evd type_of_lemma in
 	   observe (str "type_of_lemma := " ++ Printer.pr_leconstr_env (Global.env ()) !evd type_of_lemma);
 	   type_of_lemma,type_info
 	)
@@ -838,7 +832,7 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list
 	 let type_of_lemma =
 	   EConstr.it_mkProd_or_LetIn type_of_lemma_concl type_of_lemma_ctxt
 	 in
-	 let type_of_lemma = nf_zeta type_of_lemma in
+         let type_of_lemma = Reductionops.nf_zeta env !evd type_of_lemma in
          observe (str "type_of_lemma := " ++ Printer.pr_leconstr_env env !evd type_of_lemma);
 	 type_of_lemma,type_info
 	)
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index f9df3aed45..63a3e0582d 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -103,21 +103,6 @@ let const_of_ref = function
     ConstRef kn -> kn
   | _ -> anomaly (Pp.str "ConstRef expected.")
 
-
-let nf_zeta env =
-  Reductionops.clos_norm_flags  (CClosure.RedFlags.mkflags [CClosure.RedFlags.fZETA])
-    env (Evd.from_env env)
-
-
-let nf_betaiotazeta = (* Reductionops.local_strong Reductionops.whd_betaiotazeta  *)
-  Reductionops.clos_norm_flags CClosure.betaiotazeta  Environ.empty_env
-    (Evd.from_env Environ.empty_env)
-
-
-
-
-
-
 (* Generic values *)
 let pf_get_new_ids idl g =
   let ids = pf_ids_of_hyps g in
@@ -747,7 +732,7 @@ let terminate_case next_step (ci,a,t,l) expr_info continuation_tac infos g =
     with 
       | UserError(Some "Refiner.thensn_tac3",_) 
       | UserError(Some "Refiner.tclFAIL_s",_) ->
-        (observe_tac (str "is computable " ++ Printer.pr_leconstr_env (pf_env g) sigma new_info.info) (next_step continuation_tac {new_info with info = nf_betaiotazeta new_info.info} )
+        (observe_tac (str "is computable " ++ Printer.pr_leconstr_env (pf_env g) sigma new_info.info) (next_step continuation_tac {new_info with info = Reductionops.nf_betaiotazeta (pf_env g) sigma new_info.info} )
 	))
     g
     
@@ -1537,13 +1522,13 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
   (* Pp.msgnl (str "function type := " ++ Printer.pr_lconstr function_type);  *)
   let evd, ty = interp_type_evars env evd ~impls:rec_impls eq in
   let evd = Evd.minimize_universes evd in
-  let equation_lemma_type = nf_betaiotazeta (Evarutil.nf_evar evd ty) in
+  let equation_lemma_type = Reductionops.nf_betaiotazeta env evd (Evarutil.nf_evar evd ty) in
   let function_type = EConstr.to_constr ~abort_on_undefined_evars:false evd function_type in
   let equation_lemma_type = EConstr.Unsafe.to_constr equation_lemma_type in
  (* Pp.msgnl (str "lemma type := " ++ Printer.pr_lconstr equation_lemma_type ++ fnl ()); *)
   let res_vars,eq' = decompose_prod equation_lemma_type in
   let env_eq' = Environ.push_rel_context (List.map (fun (x,y) -> LocalAssum (x,y)) res_vars) env in
-  let eq' = nf_zeta env_eq' (EConstr.of_constr eq') in
+  let eq' = Reductionops.nf_zeta env_eq' evd (EConstr.of_constr eq') in
   let eq' = EConstr.Unsafe.to_constr eq' in
   let res =
 (*     Pp.msgnl (str "res_var :=" ++ Printer.pr_lconstr_env (push_rel_context (List.map (function (x,t) -> (x,None,t)) res_vars) env) eq'); *)
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index 16cff420bd..0f88734caf 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -353,7 +353,7 @@ let extend_atomic_tactic name entries =
       let default = epsilon_value inj e in
       match default with
       | None -> raise NonEmptyArgument
-      | Some def -> Tacintern.intern_tactic_or_tacarg Tacintern.fully_empty_glob_sign def
+      | Some def -> Tacintern.intern_tactic_or_tacarg (Genintern.empty_glob_sign Environ.empty_env) def
     in
     try Some (hd, List.map empty_value rem) with NonEmptyArgument -> None
   in
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index 55412c74bb..fcbcfae115 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -46,7 +46,6 @@ type glob_sign = Genintern.glob_sign = {
   extra : Genintern.Store.t;
 }
 
-let fully_empty_glob_sign = Genintern.empty_glob_sign Environ.empty_env
 let make_empty_glob_sign () = Genintern.empty_glob_sign (Global.env ())
 
 (* We have identifier <| global_reference <| constr *)
@@ -83,7 +82,8 @@ let intern_hyp ist ({loc;v=id} as locid) =
   else if find_ident id ist then
     make id
   else
-    Pretype_errors.error_var_not_found ?loc id
+    CErrors.user_err ?loc Pp.(str "Hypothesis" ++ spc () ++ Id.print id ++ spc() ++
+                              str "was not found in the current environment.")
 
 let intern_or_var f ist = function
   | ArgVar locid -> ArgVar (intern_hyp ist locid)
diff --git a/plugins/ltac/tacintern.mli b/plugins/ltac/tacintern.mli
index 9146fced2d..a9f2d76e30 100644
--- a/plugins/ltac/tacintern.mli
+++ b/plugins/ltac/tacintern.mli
@@ -23,10 +23,8 @@ type glob_sign = Genintern.glob_sign = {
   extra : Genintern.Store.t;
 }
 
-val fully_empty_glob_sign : glob_sign
-
 val make_empty_glob_sign : unit -> glob_sign
- (** same as [fully_empty_glob_sign], but with [Global.env()] as
+ (** build an empty [glob_sign] using [Global.env()] as
      environment *)
 
 (** Main globalization functions *)
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index b60b77595b..528d7de549 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -2024,7 +2024,7 @@ let interp_ltac_constr ist c k = Ftactic.run (interp_ltac_constr ist c) k
 
 let interp_redexp env sigma r =
   let ist = default_ist () in
-  let gist = { fully_empty_glob_sign with genv = env; } in
+  let gist = Genintern.empty_glob_sign env in
   interp_red_expr ist env sigma (intern_red_expr gist r)
 
 (***************************************************************************)
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index a284c3bfc7..5d75b28539 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -940,7 +940,7 @@ let pf_saturate ?beta ?bi_types gl c ?ty m =
 
 let pf_partial_solution gl t evl =
   let sigma, g = project gl, sig_it gl in
-  let sigma = Goal.V82.partial_solution sigma g t in
+  let sigma = Goal.V82.partial_solution (pf_env gl) sigma g t in
   re_sig (List.map (fun x -> (fst (EConstr.destEvar sigma x))) evl) sigma
 
 let dependent_apply_error =
diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml
index c04ced4ab4..036b20bfcd 100644
--- a/plugins/ssr/ssrequality.ml
+++ b/plugins/ssr/ssrequality.ml
@@ -433,15 +433,15 @@ let lz_coq_prod =
 
 let lz_setoid_relation =
   let sdir = ["Classes"; "RelationClasses"] in
-  let last_srel = ref (Environ.empty_env, None) in
+  let last_srel = ref None in
   fun env -> match !last_srel with
-  | env', srel when env' == env -> srel
+  | Some (env', srel) when env' == env -> srel
   | _ ->
     let srel =
        try Some (UnivGen.constr_of_global @@
                  Coqlib.find_reference "Class_setoid" ("Coq"::sdir) "RewriteRelation" [@ocaml.warning "-3"])
        with _ -> None in
-    last_srel := (env, srel); srel
+    last_srel := Some (env, srel); srel
 
 let ssr_is_setoid env =
   match lz_setoid_relation env with
diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml
index 7f67487f5d..bb6decd848 100644
--- a/plugins/ssrmatching/ssrmatching.ml
+++ b/plugins/ssrmatching/ssrmatching.ml
@@ -1048,7 +1048,7 @@ let thin id sigma goal =
   | None -> sigma
   | Some (sigma, hyps, concl) ->
     let (gl,ev,sigma) = Goal.V82.mk_goal sigma hyps concl in
-    let sigma = Goal.V82.partial_solution_to sigma goal gl ev in
+    let sigma = Goal.V82.partial_solution_to env sigma goal gl ev in
     sigma
 
 (*
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index 856894d9a6..01b0d96f98 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -164,8 +164,8 @@ let error_not_product ?loc env sigma c =
 
 (*s Error in conversion from AST to glob_constr *)
 
-let error_var_not_found ?loc s =
-  raise_pretype_error ?loc (empty_env, Evd.from_env empty_env, VarNotFound s)
+let error_var_not_found ?loc env sigma s =
+  raise_pretype_error ?loc (env, sigma, VarNotFound s)
 
 (*s Typeclass errors *)
 
diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli
index 6f14d025c7..054f0c76a9 100644
--- a/pretyping/pretype_errors.mli
+++ b/pretyping/pretype_errors.mli
@@ -150,9 +150,7 @@ val error_unexpected_type :
 val error_not_product :
   ?loc:Loc.t -> env -> Evd.evar_map -> constr -> 'b
 
-(** {6 Error in conversion from AST to glob_constr } *)
-
-val error_var_not_found : ?loc:Loc.t -> Id.t -> 'b
+val error_var_not_found : ?loc:Loc.t -> env -> Evd.evar_map -> Id.t -> 'b
 
 (** {6 Typeclass errors } *)
 
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 37afcf75e1..55817f1b76 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -390,7 +390,7 @@ let pretype_id pretype k0 loc env sigma id =
     sigma, { uj_val  = mkVar id; uj_type = NamedDecl.get_type (lookup_named id !!env) }
   with Not_found ->
     (* [id] not found, standard error message *)
-    error_var_not_found ?loc id
+    error_var_not_found ?loc !!env sigma id
 
 (*************************************************************************)
 (* Main pretyping function                                               *)
@@ -436,7 +436,7 @@ let pretype_ref ?loc sigma env ref us =
          (* This may happen if env is a goal env and section variables have
             been cleared - section variables should be different from goal
             variables *)
-         Pretype_errors.error_var_not_found ?loc id)
+         Pretype_errors.error_var_not_found ?loc !!env sigma id)
   | ref ->
     let sigma, c = pretype_global ?loc univ_flexible env sigma ref us in
     let ty = unsafe_type_of !!env sigma c in
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 367a48cb5e..aced97e910 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -1251,6 +1251,7 @@ let clos_whd_flags flgs env sigma t =
 let nf_beta = clos_norm_flags CClosure.beta
 let nf_betaiota = clos_norm_flags CClosure.betaiota
 let nf_betaiotazeta = clos_norm_flags CClosure.betaiotazeta
+let nf_zeta = clos_norm_flags CClosure.zeta
 let nf_all env sigma =
   clos_norm_flags CClosure.all env sigma
 
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index c0ff6723f6..41de779414 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -171,6 +171,7 @@ val clos_whd_flags : CClosure.RedFlags.reds -> reduction_function
 val nf_beta : reduction_function
 val nf_betaiota : reduction_function
 val nf_betaiotazeta : reduction_function
+val nf_zeta : reduction_function
 val nf_all : reduction_function
 val nf_evar : evar_map -> constr -> constr
 
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 8911a2f343..4ec8569dd8 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -1135,8 +1135,8 @@ let fold_commands cl env sigma c =
 let cbv_norm_flags flags env sigma t =
   cbv_norm (create_cbv_infos flags env sigma) t
 
-let cbv_beta = cbv_norm_flags beta empty_env
-let cbv_betaiota = cbv_norm_flags betaiota empty_env
+let cbv_beta = cbv_norm_flags beta
+let cbv_betaiota = cbv_norm_flags betaiota
 let cbv_betadeltaiota env sigma =  cbv_norm_flags all env sigma
 
 let compute = cbv_betadeltaiota
diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli
index bf38c30a1f..0887d0efd3 100644
--- a/pretyping/tacred.mli
+++ b/pretyping/tacred.mli
@@ -69,8 +69,8 @@ val pattern_occs : (occurrences * constr) list -> e_reduction_function
 
 (** Call by value strategy (uses Closures) *)
 val cbv_norm_flags : CClosure.RedFlags.reds ->  reduction_function
-  val cbv_beta : local_reduction_function
-  val cbv_betaiota : local_reduction_function
+  val cbv_beta : reduction_function
+  val cbv_betaiota : reduction_function
   val cbv_betadeltaiota :  reduction_function
   val compute :  reduction_function  (** = [cbv_betadeltaiota] *)
 
diff --git a/proofs/goal.ml b/proofs/goal.ml
index 4e540de538..7245d4a004 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -72,18 +72,18 @@ module V82 = struct
     (evk, ev, evars)
 
   (* Instantiates a goal with an open term *)
-  let partial_solution sigma evk c =
+  let partial_solution env sigma evk c =
     (* Check that the goal itself does not appear in the refined term *)
     let _ =
       if not (Evarutil.occur_evar_upto sigma evk c) then ()
-      else Pretype_errors.error_occur_check Environ.empty_env sigma evk c
+      else Pretype_errors.error_occur_check env sigma evk c
     in
     Evd.define evk c sigma
 
   (* Instantiates a goal with an open term, using name of goal for evk' *)
-  let partial_solution_to sigma evk evk' c =
+  let partial_solution_to env sigma evk evk' c =
     let id = Evd.evar_ident evk sigma in
-    let sigma = partial_solution sigma evk c in
+    let sigma = partial_solution env sigma evk c in
     match id with
     | None -> sigma
     | Some id -> Evd.rename evk' id sigma
diff --git a/proofs/goal.mli b/proofs/goal.mli
index 3b31cff8d7..af9fb662bf 100644
--- a/proofs/goal.mli
+++ b/proofs/goal.mli
@@ -48,11 +48,11 @@ module V82 : sig
                          goal * EConstr.constr * Evd.evar_map
 
   (* Instantiates a goal with an open term *)
-  val partial_solution : Evd.evar_map -> goal -> EConstr.constr -> Evd.evar_map
+  val partial_solution : Environ.env -> Evd.evar_map -> goal -> EConstr.constr -> Evd.evar_map
 
   (* Instantiates a goal with an open term, reusing name of goal for
      second goal *)
-  val partial_solution_to : Evd.evar_map -> goal -> goal -> EConstr.constr -> Evd.evar_map
+  val partial_solution_to : Environ.env -> Evd.evar_map -> goal -> goal -> EConstr.constr -> Evd.evar_map
 
   (* Principal part of the progress tactical *)
   val progress : goal list Evd.sigma -> goal Evd.sigma -> bool
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 254c93d0a2..b8612cd2c0 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -590,5 +590,5 @@ let prim_refiner r sigma goal =
         check_meta_variables env sigma c;
 	let (sgl,cl',sigma,oterm) = mk_refgoals sigma goal [] cl c in
 	let sgl = List.rev sgl in
-	let sigma = Goal.V82.partial_solution sigma goal (EConstr.of_constr oterm) in
+        let sigma = Goal.V82.partial_solution env sigma goal (EConstr.of_constr oterm) in
 	  (sgl, sigma)