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

5 files changed, 11 insertions, 11 deletions

diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index 6b5cb7492..db53dc932 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
diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index 0acdc4c80..d34edb863 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -150,7 +150,7 @@ let left_instance_tac (inst,id) continue seq=
 		Proofview.V82.of_tactic introf;
 		tclSOLVE [wrap 1 false continue
 			    (deepen (record (id,None) seq))]];
-	    tclTRY assumption]
+	    tclTRY (Proofview.V82.of_tactic assumption)]
     | Real((m,t) as c,_)->
 	if lookup (id,Some c) seq then
 	  tclFAIL 0 (Pp.str "already done")
@@ -182,7 +182,7 @@ let right_instance_tac inst continue seq=
 	       Proofview.V82.of_tactic (split (ImplicitBindings
 			[mkVar (Tacmach.pf_nth_hyp_id gls 1)])) gls);
 	    tclSOLVE [wrap 0 true continue (deepen seq)]];
-	 tclTRY assumption]
+	 tclTRY (Proofview.V82.of_tactic assumption)]
     | Real ((0,t),_) ->
 	(tclTHEN (Proofview.V82.of_tactic (split (ImplicitBindings [t])))
 	   (tclSOLVE [wrap 0 true continue (deepen seq)]))
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 8c2fdb7eb..3d74c5bc9 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -120,7 +120,7 @@ type body_info = constr dynamic_info
 
 let finish_proof dynamic_infos g =
   observe_tac "finish"
-    ( h_assumption)
+    (Proofview.V82.of_tactic h_assumption)
     g
 
 
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 881d930fc..64bf71ec6 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -517,7 +517,7 @@ let rec prove_lt hyple g =
 	(
 	  tclTHENLIST[
 	    apply (delayed_force lt_S_n);
-	    (observe_tac (str "assumption: " ++ Printer.pr_goal g) (h_assumption))
+	    (observe_tac (str "assumption: " ++ Printer.pr_goal g) (Proofview.V82.of_tactic h_assumption))
 	  ])
       )
   end
@@ -757,7 +757,7 @@ let terminate_app_rec (f,args) expr_info continuation_tac _ =
 	    tclTHENS (* proof of args < formal args *)
 	      (apply (Lazy.force expr_info.acc_inv))
 	      [ 
-		observe_tac (str "h_assumption") h_assumption;
+		observe_tac (str "h_assumption") (Proofview.V82.of_tactic h_assumption);
 		tclTHENLIST
 		  [
 		    tclTRY(list_rewrite true 
@@ -802,7 +802,7 @@ let rec prove_le g =
     (List.hd args,List.hd (List.tl args))
   in 
   tclFIRST[
-    h_assumption;
+    Proofview.V82.of_tactic h_assumption;
     apply (delayed_force le_n);
     begin
       try
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index 26d252726..98baf7b2a 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -1058,7 +1058,7 @@ let replay_history tactic_normalisation =
 		Proofview.V82.tactic (simpl_in_concl);
 		intro;
 		(absurd not_sup_sup) ])
-	      [ Proofview.V82.tactic assumption ; reflexivity ]
+	      [ assumption ; reflexivity ]
 	  in
 	  let theorem =
             mkApp (Lazy.force coq_OMEGA2, [|
@@ -1127,7 +1127,7 @@ let replay_history tactic_normalisation =
 		  (intros_using [aux]);
 		  Proofview.V82.tactic (resolve_id aux);
 		  Proofview.V82.tactic (mk_then tac);
-		  Proofview.V82.tactic assumption ] ;
+		  assumption ] ;
 		 Tacticals.New.tclTHENLIST [
 		   Proofview.V82.tactic (unfold sp_Zgt);
 		   Proofview.V82.tactic simpl_in_concl;