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/decl_mode/decl_proof_instr.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/decl_mode')

diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index 9d64efdeda..4bc60fffff 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -712,7 +712,7 @@ let rec consider_match may_intro introduced available expected gls =
 		  consider_match may_intro ((id,false)::introduced) rest_ids rest
 	      | Name hid ->
 		  tclTHENLIST
-		    [rename_hyp [id,hid];
+		    [Proofview.V82.of_tactic (rename_hyp [id,hid]);
 		     consider_match may_intro ((hid,true)::introduced) rest_ids rest]
 	  end
 	  begin
-- 
cgit v1.2.3