diff options
-rw-r--r-- | plugins/decl_mode/decl_proof_instr.ml | 6 | ||||
-rw-r--r-- | plugins/firstorder/instances.ml | 4 | ||||
-rw-r--r-- | plugins/funind/functional_principles_proofs.ml | 2 | ||||
-rw-r--r-- | plugins/funind/recdef.ml | 6 | ||||
-rw-r--r-- | plugins/omega/coq_omega.ml | 4 | ||||
-rw-r--r-- | tactics/auto.ml | 6 | ||||
-rw-r--r-- | tactics/contradiction.ml | 2 | ||||
-rw-r--r-- | tactics/equality.ml | 4 | ||||
-rw-r--r-- | tactics/hiddentac.mli | 2 | ||||
-rw-r--r-- | tactics/rewrite.ml | 2 | ||||
-rw-r--r-- | tactics/tacinterp.ml | 2 | ||||
-rw-r--r-- | tactics/tactics.ml | 45 | ||||
-rw-r--r-- | tactics/tactics.mli | 2 |
13 files changed, 52 insertions, 35 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; diff --git a/tactics/auto.ml b/tactics/auto.ml index 1205d9700..e87158bdd 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -1270,7 +1270,7 @@ let exists_evaluable_reference env = function | EvalVarRef v -> try ignore(lookup_named v env); true with Not_found -> false let dbg_intro dbg = new_tclLOG dbg (fun () -> str "intro") intro -let dbg_assumption dbg = tclLOG dbg (fun () -> str "assumption") assumption +let dbg_assumption dbg = new_tclLOG dbg (fun () -> str "assumption") assumption let rec trivial_fail_db dbg mod_delta db_list local_db = let intro_tac = @@ -1286,7 +1286,7 @@ let rec trivial_fail_db dbg mod_delta db_list local_db = Proofview.Goal.enter begin fun gl -> let concl = Proofview.Goal.concl gl in Tacticals.New.tclFIRST - ((Proofview.V82.tactic (dbg_assumption dbg))::intro_tac:: + ((dbg_assumption dbg)::intro_tac:: (List.map Tacticals.New.tclCOMPLETE (trivial_resolve dbg mod_delta db_list local_db concl))) end @@ -1441,7 +1441,7 @@ let search d n mod_delta db_list local_db = each goal. Hence the [tclEXTEND] *) Proofview.tclEXTEND [] begin if Int.equal n 0 then Proofview.tclZERO (Errors.UserError ("",str"BOUND 2")) else - Tacticals.New.tclORELSE0 (Proofview.V82.tactic (dbg_assumption d)) + Tacticals.New.tclORELSE0 (dbg_assumption d) (Tacticals.New.tclORELSE0 (intro_register d (search d n) local_db) ( Proofview.Goal.enter begin fun gl -> let concl = Proofview.Goal.concl gl in diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml index 19e5906f8..0198fc3fd 100644 --- a/tactics/contradiction.ml +++ b/tactics/contradiction.ml @@ -91,7 +91,7 @@ let contradiction_term (c,lbind as cl) = let typ = type_of c in let _, ccl = splay_prod env sigma typ in if is_empty_type ccl then - Tacticals.New.tclTHEN (elim false cl None) (Proofview.V82.tactic (tclTRY assumption)) + Tacticals.New.tclTHEN (elim false cl None) (Tacticals.New.tclTRY assumption) else Proofview.tclORELSE begin diff --git a/tactics/equality.ml b/tactics/equality.ml index 36cb55e5b..7c72d8ad5 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -531,8 +531,8 @@ let multi_replace clause c2 c1 unsafe try_prove_eq_opt = (Tacticals.New.tclTRY (general_multi_rewrite false false (mkVar id,NoBindings) clause)) (Proofview.V82.tactic (clear [id]))); Tacticals.New.tclFIRST - [Proofview.V82.tactic assumption; - Tacticals.New.tclTHEN (Proofview.V82.tactic (apply sym)) (Proofview.V82.tactic assumption); + [assumption; + Tacticals.New.tclTHEN (Proofview.V82.tactic (apply sym)) assumption; try_prove_eq ] ] diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli index f81698370..ad7654374 100644 --- a/tactics/hiddentac.mli +++ b/tactics/hiddentac.mli @@ -29,7 +29,7 @@ val h_intro_move : Id.t option -> Id.t move_location -> unit Proofview.tact val h_intro : Id.t -> unit Proofview.tactic val h_intros_until : quantified_hypothesis -> unit Proofview.tactic -val h_assumption : tactic +val h_assumption : unit Proofview.tactic val h_exact : constr -> tactic val h_exact_no_check : constr -> tactic val h_vm_cast_no_check : constr -> tactic diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml index f40ec7659..337ae5241 100644 --- a/tactics/rewrite.ml +++ b/tactics/rewrite.ml @@ -1835,7 +1835,7 @@ let setoid_symmetry_in id = let new_hyp = it_mkProd_or_LetIn new_hyp' binders in Tacticals.New.tclTHENS (Proofview.V82.tactic (Tactics.cut new_hyp)) [ Proofview.V82.tactic (intro_replacing id); - Tacticals.New.tclTHENLIST [ intros; setoid_symmetry; Proofview.V82.tactic (apply (mkVar id)); Proofview.V82.tactic (Tactics.assumption) ] ] + Tacticals.New.tclTHENLIST [ intros; setoid_symmetry; Proofview.V82.tactic (apply (mkVar id)); Tactics.assumption ] ] end let _ = Hook.set Tactics.setoid_reflexivity setoid_reflexivity diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 34314088c..248a5d36b 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1756,7 +1756,7 @@ and interp_atomic ist tac = let mloc = Tacmach.New.of_old (fun gl -> interp_move_location ist gl hto) gl in h_intro_move (Option.map (interp_fresh_ident ist env) ido) mloc end - | TacAssumption -> Proofview.V82.tactic h_assumption + | TacAssumption -> h_assumption | TacExact c -> Proofview.V82.tactic begin fun gl -> let (sigma,c_interp) = pf_interp_casted_constr ist gl c in diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 0bf295b3c..2f52c8b7a 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1166,19 +1166,36 @@ let exact_proof c gl = let c = Constrintern.interp_casted_constr (project gl) (pf_env gl) c (pf_concl gl) in refine_no_check c gl -let (assumption : tactic) = fun gl -> - let concl = pf_concl gl in - let hyps = pf_hyps gl in - let rec arec only_eq = function - | [] -> - if only_eq then arec false hyps else error "No such assumption." - | (id,c,t)::rest -> - if (only_eq && eq_constr t concl) - || (not only_eq && pf_conv_x_leq gl t concl) - then refine_no_check (mkVar id) gl - else arec only_eq rest +let tclZEROMSG msg = + Proofview.tclZERO (UserError ("", msg)) + +let assumption = + let rec arec gl only_eq = function + | [] -> + if only_eq then + let hyps = Proofview.Goal.hyps gl in + arec gl false hyps + else tclZEROMSG (str "No such assumption.") + | (id, c, t)::rest -> + let concl = Proofview.Goal.concl gl in + let is_same_type = + if only_eq then eq_constr t concl + else + let sigma = Proofview.Goal.sigma gl in + let env = Proofview.Goal.env gl in + is_conv_leq env sigma t concl + in + if is_same_type then + let c = Goal.Refinable.make (fun _ -> Goal.return (mkVar id)) in + let r = Goal.bind c Goal.refine in + Proofview.tclSENSITIVE r + else arec gl only_eq rest + in + let assumption_tac gl = + let hyps = Proofview.Goal.hyps gl in + arec gl true hyps in - arec true hyps + Proofview.Goal.enter assumption_tac (*****************************************************************) (* Modification of a local context *) @@ -3688,7 +3705,7 @@ let symmetry_in id = | HeterogenousEq (t1,c1,t2,c2) -> mkApp (hdcncl, [| t2; c2; t1; c1 |]) in Tacticals.New.tclTHENS (Proofview.V82.tactic (cut (it_mkProd_or_LetIn symccl sign))) [ Proofview.V82.tactic (intro_replacing id); - Tacticals.New.tclTHENLIST [ intros; symmetry; Proofview.V82.tactic (apply (mkVar id)); Proofview.V82.tactic assumption ] ] + Tacticals.New.tclTHENLIST [ intros; symmetry; Proofview.V82.tactic (apply (mkVar id)); assumption ] ] end begin function | NoEquationFound -> Hook.get forward_setoid_symmetry_in id @@ -3739,7 +3756,7 @@ let prove_transitivity hdcncl eq_kind t = (Tacticals.New.tclTHENLIST [ Tacticals.New.tclDO 2 intro; Tacticals.New.onLastHyp simplest_case; - Proofview.V82.tactic assumption ])) + assumption ])) end let transitivity_red allowred t = diff --git a/tactics/tactics.mli b/tactics/tactics.mli index fc4c780fe..c3df47215 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -120,7 +120,7 @@ val intros_pattern : (** {6 Exact tactics. } *) -val assumption : tactic +val assumption : unit Proofview.tactic val exact_no_check : constr -> tactic val vm_cast_no_check : constr -> tactic val exact_check : constr -> tactic |