Change reduction_of_red_expr to return an e_reduction_function returning

an updated evar_map, as pattern is working up to universe equalities
that must be kept. Straightforward adaptation of the code depending on
this.

14 files changed, 77 insertions, 38 deletions

diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml
index a28a46c74..6abf96dce 100644
--- a/plugins/btauto/refl_btauto.ml
+++ b/plugins/btauto/refl_btauto.ml
@@ -179,7 +179,7 @@ module Btauto = struct
   let print_counterexample p env gl =
     let var = lapp witness [|p|] in
     (* Compute an assignment that dissatisfies the goal *)
-    let var = Tacmach.pf_reduction_of_red_expr gl (Genredexpr.CbvVm None) var in
+    let _, var = Tacmach.pf_reduction_of_red_expr gl (Genredexpr.CbvVm None) var in
     let rec to_list l = match decomp_term l with
     | Term.App (c, _)
       when c === (Lazy.force CoqList._nil) -> []
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index ca9f995f1..0d254c9af 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -675,7 +675,7 @@ let mkDestructEq :
       (fun g2 ->
 	change_in_concl None
 	  (fun env sigma -> 
-	    sigma, pattern_occs [Locus.AllOccurrencesBut [1], expr] (pf_env g2) Evd.empty (pf_concl g2)) g2);
+	    pattern_occs [Locus.AllOccurrencesBut [1], expr] (pf_env g2) sigma (pf_concl g2)) g2);
       Proofview.V82.of_tactic (simplest_case expr)]), to_revert
 
 
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 150ff93ce..b2938cb99 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -1124,21 +1124,21 @@ let compute = cbv_betadeltaiota
 (* gives [na:ta]c' such that c converts to ([na:ta]c' a), abstracting only
  * the specified occurrences. *)
 
-let abstract_scheme env sigma (locc,a) c =
+let abstract_scheme env (locc,a) (c, sigma) =
   let ta = Retyping.get_type_of env sigma a in
   let na = named_hd env ta Anonymous in
   if occur_meta ta then error "Cannot find a type for the generalisation.";
   if occur_meta a then
-    mkLambda (na,ta,c)
+    mkLambda (na,ta,c), sigma
   else
     let c', sigma' = subst_closed_term_occ env sigma locc a c in
-      mkLambda (na,ta,c') 
+      mkLambda (na,ta,c'), sigma'
 
 let pattern_occs loccs_trm env sigma c =
-  let abstr_trm = List.fold_right (abstract_scheme env sigma) loccs_trm c in
+  let abstr_trm, sigma = List.fold_right (abstract_scheme env) loccs_trm (c,sigma) in
   try
     let _ = Typing.type_of env sigma abstr_trm in
-    applist(abstr_trm, List.map snd loccs_trm)
+      sigma, applist(abstr_trm, List.map snd loccs_trm)
   with Type_errors.TypeError (env',t) ->
     raise (ReductionTacticError (InvalidAbstraction (env,sigma,abstr_trm,(env',t))))
 
diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli
index db59787a1..6e0479fb1 100644
--- a/pretyping/tacred.mli
+++ b/pretyping/tacred.mli
@@ -62,7 +62,7 @@ val fold_commands : constr list ->  reduction_function
 
 (** Pattern *)
 val pattern_occs : (occurrences * constr) list -> env -> evar_map -> constr -> 
-  constr
+   evar_map * constr
 
 (** Rem: Lazy strategies are defined in Reduction *)
 
diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index 4db853ee8..acdc52400 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -175,25 +175,28 @@ let out_with_occurrences (occs,c) =
 
 let reduction_of_red_expr env =
   let make_flag = make_flag env in
+  let e_red f env evm c = evm, f env evm c in
   let rec reduction_of_red_expr = function
   | Red internal ->
-      if internal then (try_red_product,DEFAULTcast)
-      else (red_product,DEFAULTcast)
-  | Hnf -> (hnf_constr,DEFAULTcast)
+      if internal then (e_red try_red_product,DEFAULTcast)
+      else (e_red red_product,DEFAULTcast)
+  | Hnf -> (e_red hnf_constr,DEFAULTcast)
   | Simpl (Some (_,c as lp)) ->
-    (contextually (is_reference c) (out_with_occurrences lp)
-      (fun _ -> simpl),DEFAULTcast)
-  | Simpl None -> (simpl,DEFAULTcast)
-  | Cbv f -> (cbv_norm_flags (make_flag f),DEFAULTcast)
+    let f = contextually (is_reference c) (out_with_occurrences lp)
+      (fun _ -> simpl)
+    in (e_red f,DEFAULTcast)
+  | Simpl None -> (e_red simpl,DEFAULTcast)
+  | Cbv f -> (e_red (cbv_norm_flags (make_flag f)),DEFAULTcast)
   | Cbn f ->
-    (strong (fun env evd x -> Stack.zip ~refold:true
-      (fst (whd_state_gen true (make_flag f) env evd (x, Stack.empty)))),DEFAULTcast)
-  | Lazy f -> (clos_norm_flags (make_flag f),DEFAULTcast)
-  | Unfold ubinds -> (unfoldn (List.map out_with_occurrences ubinds),DEFAULTcast)
-  | Fold cl -> (fold_commands cl,DEFAULTcast)
+    let f = strong (fun env evd x -> Stack.zip ~refold:true
+      (fst (whd_state_gen true (make_flag f) env evd (x, Stack.empty)))) in
+      (e_red f, DEFAULTcast)
+  | Lazy f -> (e_red (clos_norm_flags (make_flag f)),DEFAULTcast)
+  | Unfold ubinds -> (e_red (unfoldn (List.map out_with_occurrences ubinds)),DEFAULTcast)
+  | Fold cl -> (e_red (fold_commands cl),DEFAULTcast)
   | Pattern lp -> (pattern_occs (List.map out_with_occurrences lp),DEFAULTcast)
   | ExtraRedExpr s ->
-      (try (String.Map.find s !reduction_tab,DEFAULTcast)
+      (try (e_red (String.Map.find s !reduction_tab),DEFAULTcast)
       with Not_found ->
 	(try reduction_of_red_expr (String.Map.find s !red_expr_tab)
 	 with Not_found ->
@@ -206,8 +209,8 @@ let reduction_of_red_expr env =
       Vnorm.cbv_vm env c tpe
     in
     let redfun = contextually b lp vmfun in
-    (redfun, VMcast)
-  | CbvVm None -> (cbv_vm, VMcast)
+    (e_red redfun, VMcast)
+  | CbvVm None -> (e_red cbv_vm, VMcast)
   | CbvNative (Some lp) ->
     let b = is_reference (snd lp) in
     let lp = out_with_occurrences lp in
@@ -217,8 +220,8 @@ let reduction_of_red_expr env =
       Nativenorm.native_norm env evars c tpe
     in
     let redfun = contextually b lp nativefun in
-    (redfun, NATIVEcast)
-  | CbvNative None -> (cbv_native, NATIVEcast)
+    (e_red redfun, NATIVEcast)
+  | CbvNative None -> (e_red cbv_native, NATIVEcast)
   in
     reduction_of_red_expr
 
diff --git a/proofs/redexpr.mli b/proofs/redexpr.mli
index 755497615..f4963eec5 100644
--- a/proofs/redexpr.mli
+++ b/proofs/redexpr.mli
@@ -19,7 +19,7 @@ type red_expr =
 val out_with_occurrences : 'a with_occurrences -> occurrences * 'a
 
 val reduction_of_red_expr :
-  Environ.env -> red_expr -> reduction_function * cast_kind
+  Environ.env -> red_expr -> e_reduction_function * cast_kind
 
 (** [true] if we should use the vm to verify the reduction *)
 
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index c6f09eb2d..7349a8273 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -76,6 +76,7 @@ let pf_apply f gls = f (pf_env gls) (project gls)
 let pf_eapply f gls x = 
   on_sig gls (fun evm -> f (pf_env gls) evm x)
 let pf_reduce = pf_apply
+let pf_e_reduce = pf_apply
 
 let pf_whd_betadeltaiota         = pf_reduce whd_betadeltaiota
 let pf_hnf_constr                = pf_reduce hnf_constr
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index b754f6f40..3ee970c1f 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -50,7 +50,7 @@ val pf_get_hyp_typ        : goal sigma -> Id.t -> types
 val pf_get_new_id  : Id.t      -> goal sigma -> Id.t
 val pf_get_new_ids : Id.t list -> goal sigma -> Id.t list
 
-val pf_reduction_of_red_expr : goal sigma -> red_expr -> constr -> constr
+val pf_reduction_of_red_expr : goal sigma -> red_expr -> constr -> evar_map * constr
 
 
 val pf_apply : (env -> evar_map -> 'a) -> goal sigma -> 'a
@@ -59,6 +59,9 @@ val pf_eapply : (env -> evar_map -> 'a -> evar_map * 'b) ->
 val pf_reduce :
   (env -> evar_map -> constr -> constr) ->
   goal sigma -> constr -> constr
+val pf_e_reduce :
+  (env -> evar_map -> constr -> evar_map * constr) ->
+  goal sigma -> constr -> evar_map * constr
 
 val pf_whd_betadeltaiota       : goal sigma -> constr -> constr
 val pf_hnf_constr              : goal sigma -> constr -> constr
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index bce768cd4..d048d5bcd 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -706,7 +706,7 @@ let  mkCaseEq a  : unit Proofview.tactic =
             let env = Proofview.Goal.env gl in
             Proofview.V82.tactic begin
 	      change_concl
-	        (Tacred.pattern_occs [Locus.OnlyOccurrences [1], a] env Evd.empty concl)
+	        (snd (Tacred.pattern_occs [Locus.OnlyOccurrences [1], a] env Evd.empty concl))
             end
           end;
 	  simplest_case a]
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index 1e3996429..c79f8b35f 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -1324,12 +1324,13 @@ module Strategies =
     let reduce (r : Redexpr.red_expr) : 'a pure_strategy =
 	fun state env avoid t ty cstr evars ->
           let rfn, ckind = Redexpr.reduction_of_red_expr env r in
-	  let t' = rfn env (goalevars evars) t in
+	  let evars', t' = rfn env (goalevars evars) t in
 	    if eq_constr t' t then
 	      state, Identity
 	    else
 	      state, Success { rew_car = ty; rew_from = t; rew_to = t';
-				  rew_prf = RewCast ckind; rew_evars = evars }
+			       rew_prf = RewCast ckind; 
+			       rew_evars = evars', cstrevars evars }
 	
     let fold_glob c : 'a pure_strategy =
       fun state env avoid t ty cstr evars ->
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 2055bd7ea..d05f5f8ad 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -681,7 +681,7 @@ let interp_may_eval f ist env sigma = function
   | ConstrEval (r,c) ->
       let (sigma,redexp) = interp_red_expr ist env sigma r in
       let (sigma,c_interp) = f ist env sigma c in
-      sigma , (fst (Redexpr.reduction_of_red_expr env redexp) env sigma c_interp)
+      (fst (Redexpr.reduction_of_red_expr env redexp) env sigma c_interp)
   | ConstrContext ((loc,s),c) ->
       (try
 	let (sigma,ic) = f ist env sigma c in
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 0875a7656..b78bb9299 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -122,7 +122,6 @@ let refine          = Tacmach.refine
 let convert_concl ?(check=true) ty k =
   Proofview.Goal.enter begin fun gl ->
     let env = Proofview.Goal.env gl in
-    let sigma = Proofview.Goal.sigma gl in
     let conclty = Proofview.Goal.raw_concl gl in
     Proofview.Refine.refine ~unsafe:true begin fun sigma ->
       let sigma =
@@ -432,6 +431,38 @@ let reduct_option ?(check=false) redfun = function
   | Some id -> reduct_in_hyp ~check (fst redfun) id
   | None    -> reduct_in_concl (revert_cast redfun)
 
+(** Tactic reduction modulo evars (for universes essentially) *)
+
+let pf_e_reduce_decl redfun where (id,c,ty) gl =
+  let sigma = project gl in
+  let redfun = redfun (pf_env gl) in
+  match c with
+  | None ->
+      if where == InHypValueOnly then
+	errorlabstrm "" (pr_id id ++ str "has no value.");
+    let sigma, ty' = redfun sigma ty in
+      sigma, (id,None,ty')
+  | Some b ->
+      let sigma, b' = if where != InHypTypeOnly then redfun sigma b else sigma, b in
+      let sigma, ty' = if where != InHypValueOnly then redfun sigma ty else sigma, ty in
+	sigma, (id,Some b',ty')
+
+let e_reduct_in_concl (redfun,sty) gl =
+  Proofview.V82.of_tactic
+    (let sigma, c' = (pf_apply redfun gl (pf_concl gl)) in
+       Proofview.Unsafe.tclEVARS sigma <*> 
+	 convert_concl_no_check c' sty) gl
+
+let e_reduct_in_hyp ?(check=false) redfun (id,where) gl =
+  Proofview.V82.of_tactic 
+    (let sigma, decl' = pf_e_reduce_decl redfun where (pf_get_hyp gl id) gl in
+       Proofview.Unsafe.tclEVARS sigma <*> 
+	 convert_hyp ~check decl') gl
+
+let e_reduct_option ?(check=false) redfun = function
+  | Some id -> e_reduct_in_hyp ~check (fst redfun) id
+  | None    -> e_reduct_in_concl (revert_cast redfun)
+
 (** Versions with evars to maintain the unification of universes resulting
     from conversions. *)
 
@@ -552,7 +583,7 @@ let normalise_vm_in_concl = reduct_in_concl (Redexpr.cbv_vm,VMcast)
 let unfold_in_concl loccname = reduct_in_concl (unfoldn loccname,REVERTcast)
 let unfold_in_hyp   loccname = reduct_in_hyp   (unfoldn loccname)
 let unfold_option   loccname = reduct_option (unfoldn loccname,DEFAULTcast)
-let pattern_option l = reduct_option (pattern_occs l,DEFAULTcast)
+let pattern_option l = e_reduct_option (pattern_occs l,DEFAULTcast)
 
 (* The main reduction function *)
 
@@ -568,7 +599,7 @@ let reduce redexp cl goal =
   let cl = concrete_clause_of (fun () -> pf_ids_of_hyps goal) cl in
   let redexps = reduction_clause redexp cl in
   let tac = tclMAP (fun (where,redexp) ->
-    reduct_option ~check:true
+    e_reduct_option ~check:true
       (Redexpr.reduction_of_red_expr (pf_env goal) redexp) where) redexps in
   match redexp with
   | Fold _ | Pattern _ -> with_check tac goal
@@ -738,8 +769,8 @@ let pf_lookup_hypothesis_as_renamed_gen red h gl =
     match pf_lookup_hypothesis_as_renamed env ccl h with
       | None when red ->
           aux
-	    ((fst (Redexpr.reduction_of_red_expr env (Red true)))
-	       env (project gl) ccl)
+	    (snd ((fst (Redexpr.reduction_of_red_expr env (Red true)))
+	       env (project gl) ccl))
       | x -> x
   in
   try aux (pf_concl gl)
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 76ea462c7..57f2571c5 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -42,7 +42,7 @@ let do_universe l = Declare.do_universe l
 let do_constraint l = Declare.do_constraint l
 
 let rec under_binders env f n c =
-  if Int.equal n 0 then f env Evd.empty c else
+  if Int.equal n 0 then snd (f env Evd.empty c) else
     match kind_of_term c with
       | Lambda (x,t,c) ->
 	  mkLambda (x,t,under_binders (push_rel (x,None,t) env) f (n-1) c)
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 74ea904c4..e04cad5c4 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1496,7 +1496,7 @@ let vernac_check_may_eval redexp glopt rc =
     | Some r ->
         Tacintern.dump_glob_red_expr r;
         let (sigma',r_interp) = interp_redexp env sigma' r in
-	let redfun = fst (reduction_of_red_expr env r_interp) in
+	let redfun env evm c = snd (fst (reduction_of_red_expr env r_interp) env evm c) in
 	msg_notice (print_eval redfun env sigma' rc j)
 
 let vernac_declare_reduction locality s r =