From d0a871374e3b3498c51d9d7b8e4510f7e1e7a3e1 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 3 Nov 2014 20:47:06 +0100
Subject: Writing rename_hyps in the new monad.

This new implementation now allows for simultaneous replacing of hypotheses,
thus fixing bug #2149.
---
 plugins/funind/functional_principles_proofs.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'plugins/funind')

diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index c530cbdeac..8e6bbcefdd 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -180,7 +180,7 @@ let change_hyp_with_using msg hyp_id t tac : tactic =
       [tclTHENLIST
       [
 	(* observe_tac "change_hyp_with_using thin" *) (thin [hyp_id]);
-	(* observe_tac "change_hyp_with_using rename " *) (rename_hyp [prov_id,hyp_id])
+	(* observe_tac "change_hyp_with_using rename " *) (Proofview.V82.of_tactic (rename_hyp [prov_id,hyp_id]))
       ]] g
 
 exception TOREMOVE
@@ -642,7 +642,7 @@ let instanciate_hyps_with_args (do_prove:Id.t list -> tactic) hyps args_id =
             Refiner.tclEVARS evm;
 	    Proofview.V82.of_tactic (pose_proof (Name prov_hid) c);
 	    thin [hid];
-	    rename_hyp [prov_hid,hid]
+	    Proofview.V82.of_tactic (rename_hyp [prov_hid,hid])
 	  ] g
       )
       ( (*
-- 
cgit v1.2.3