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 +++--- plugins/firstorder/instances.ml | 4 ++-- plugins/funind/functional_principles_proofs.ml | 2 +- plugins/funind/recdef.ml | 6 +++--- plugins/omega/coq_omega.ml | 4 ++-- 5 files changed, 11 insertions(+), 11 deletions(-) (limited to 'plugins') 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; -- cgit v1.2.3