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, 26 insertions, 19 deletions

diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index 4db853ee87..acdc524004 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 7554976155..f4963eec56 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 c6f09eb2db..7349a82730 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 b754f6f408..3ee970c1f9 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