From 5180ab68819f10949cd41a2458bff877b3ec3204 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 15 Feb 2016 16:45:18 +0100
Subject: Using monotonic types for conversion functions.

---
 plugins/funind/recdef.ml | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

(limited to 'plugins')

diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 6c6caa6284..555f08fa86 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -690,9 +690,8 @@ let mkDestructEq :
      [generalize new_hyps;
       (fun g2 ->
         let changefun patvars = { run = fun sigma ->
-          let sigma = Sigma.to_evar_map sigma in
-          let (sigma, c) = pattern_occs [Locus.AllOccurrencesBut [1], expr] (pf_env g2) sigma (pf_concl g2) in
-          Sigma.Unsafe.of_pair (c, sigma)
+          let redfun = pattern_occs [Locus.AllOccurrencesBut [1], expr] in
+          redfun.Reductionops.e_redfun (pf_env g2) sigma (pf_concl g2)
         } in
 	Proofview.V82.of_tactic (change_in_concl None changefun) g2);
       Proofview.V82.of_tactic (simplest_case expr)]), to_revert
-- 
cgit v1.2.3