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.

4 files changed, 41 insertions, 9 deletions

diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index bce768cd42..d048d5bcdb 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 1e3996429b..c79f8b35f7 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 2055bd7eab..d05f5f8adb 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 0875a76564..b78bb9299f 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)