From 884b6cc6c12bd557085cdaa4972d593684c9cc1a Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Fri, 24 Oct 2014 17:38:59 +0200
Subject: 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.

---
 plugins/btauto/refl_btauto.ml | 2 +-
 plugins/funind/recdef.ml      | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'plugins')

diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml
index a28a46c74b..6abf96dcee 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 ca9f995f15..0d254c9af7 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
 
 
-- 
cgit v1.2.3