From b3bfa1179bc6dda1a179e0ed5bc98dccdc1b3e14 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 16 May 2016 21:41:55 +0200
Subject: Put the "generalize" tactic in the monad.

---
 plugins/decl_mode/decl_proof_instr.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'plugins/decl_mode')

diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index a6b3381648..de06af0053 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -1289,7 +1289,7 @@ let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls =
 		       (fun id ->
 			  hrec_for (out_name fix_name) per_info gls1 id)
 		       recs in
-		     generalize hrecs gls1
+		     Proofview.V82.of_tactic (generalize hrecs) gls1
 	       end;
 	       match bro with
 		   None ->
@@ -1365,7 +1365,7 @@ let end_tac et2 gls =
 		(default_justification (List.map mkVar clauses))
 	  | ET_Induction,EK_nodep ->
 	      tclTHENLIST
-		[generalize (pi.per_args@[pi.per_casee]);
+		[Proofview.V82.of_tactic (generalize (pi.per_args@[pi.per_casee]));
 		 Proofview.V82.of_tactic (simple_induct (AnonHyp (succ (List.length pi.per_args))));
 		 default_justification (List.map mkVar clauses)]
 	  | ET_Case_analysis,EK_dep tree ->
@@ -1377,7 +1377,7 @@ let end_tac et2 gls =
 		   (initial_instance_stack clauses) [pi.per_casee] 0 tree
 	  | ET_Induction,EK_dep tree ->
 	      let nargs = (List.length pi.per_args) in
-		tclTHEN (generalize (pi.per_args@[pi.per_casee]))
+		tclTHEN (Proofview.V82.of_tactic (generalize (pi.per_args@[pi.per_casee])))
 		  begin
 		    fun gls0 ->
 		      let fix_id =
-- 
cgit v1.2.3