From 2fa05a8d300f5c0d375a558a8bced972eea4bfaf Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 7 Dec 2014 18:32:56 +0100
Subject: Moving change_in_concl, change_in_hyp, change_concl to
 Proofview.tactic.

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

(limited to 'plugins/funind')

diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index fd54584bc8..a38764c5bd 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -673,9 +673,9 @@ let mkDestructEq :
     tclTHENLIST
      [Simple.generalize new_hyps;
       (fun g2 ->
-	change_in_concl None
+	Proofview.V82.of_tactic (change_in_concl None
 	  (fun sigma ->
-	    pattern_occs [Locus.AllOccurrencesBut [1], expr] (pf_env g2) sigma (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