From 6cf364b18897c61b3200ed9c5795c7b48cf23b59 Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Fri, 8 Nov 2013 21:09:53 +0000
Subject: Porting Tactics.assumption to the new engine.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17073 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 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 6b5cb7492b..db53dc9320 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -243,7 +243,7 @@ let automation_tac = Proofview.tclBIND (Proofview.tclUNIT ()) (fun () -> !my_aut
 
 let justification tac gls=
     tclORELSE
-      (tclSOLVE [tclTHEN tac assumption])
+      (tclSOLVE [tclTHEN tac (Proofview.V82.of_tactic assumption)])
       (fun gls ->
 	 if get_strictness () then
 	   error "Insufficient justification."
@@ -1326,7 +1326,7 @@ let end_tac et2 gls =
 		   (fun c -> tclTHENLIST 
 		      [my_refine c;
 		       clear clauses;
-		       justification assumption])
+		       justification (Proofview.V82.of_tactic assumption)])
 		   (initial_instance_stack clauses) [pi.per_casee] 0 tree
 	  | ET_Induction,EK_dep tree ->
 	      let nargs = (List.length pi.per_args) in
@@ -1347,7 +1347,7 @@ let end_tac et2 gls =
 				  [clear [fix_id];
 				   my_refine c;
 				   clear clauses;
-				   justification assumption])
+				   justification (Proofview.V82.of_tactic assumption)])
 			     (initial_instance_stack clauses)
 			     [mkVar c_id]  0 tree] gls0
 		  end
-- 
cgit v1.2.3