diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/equality.ml | 6 | ||||
| -rw-r--r-- | tactics/tacticals.ml | 6 | ||||
| -rw-r--r-- | tactics/tacticals.mli | 1 | ||||
| -rw-r--r-- | tactics/tactics.ml | 4 |
4 files changed, 12 insertions, 5 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml index 674d01777..32563d9ff 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -533,7 +533,7 @@ let general_rewrite_clause l2r with_evars ?tac c cl = let rec do_hyps_atleastonce = function | [] -> tclZEROMSG (Pp.str"Nothing to rewrite.") | id :: l -> - tclIFTHENTRYELSEMUST + tclIFTHENFIRSTTRYELSEMUST (general_rewrite_ebindings_in l2r AllOccurrences false true ?tac id c with_evars) (do_hyps_atleastonce l) in @@ -549,7 +549,7 @@ let general_rewrite_clause l2r with_evars ?tac c cl = end in if cl.concl_occs == NoOccurrences then do_hyps else - tclIFTHENTRYELSEMUST + tclIFTHENFIRSTTRYELSEMUST (general_rewrite_ebindings l2r (occs_of cl.concl_occs) false true ?tac c with_evars) do_hyps @@ -1484,7 +1484,7 @@ let simpleInjClause flags with_evars = function | Some c -> onInductionArg (fun clear_flag -> onEquality with_evars (injEq flags ~old:true with_evars clear_flag None)) c let injConcl flags = injClause flags None false None -let injHyp flags clear_flag id = injClause flags None false (Some (clear_flag,ElimOnIdent (Loc.tag id))) +let injHyp flags clear_flag id = injClause flags None false (Some (clear_flag,ElimOnIdent CAst.(make id))) let decompEqThen keep_proofs ntac (lbeq,_,(t,t1,t2) as u) clause = Proofview.Goal.enter begin fun gl -> diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index e7da17cff..0cc0001c1 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -408,8 +408,14 @@ module New = struct Proofview.tclIFCATCH t1 (fun () -> tclDISPATCH (Array.to_list a)) (fun _ -> t3) + let tclIFTHENFIRSTELSE t1 t2 t3 = + Proofview.tclIFCATCH t1 + (fun () -> tclEXTEND [t2] (tclUNIT ()) []) + (fun _ -> t3) let tclIFTHENTRYELSEMUST t1 t2 = tclIFTHENELSE t1 (tclTRY t2) t2 + let tclIFTHENFIRSTTRYELSEMUST t1 t2 = + tclIFTHENFIRSTELSE t1 (tclTRY t2) t2 (* Try the first tactic that does not fail in a list of tactics *) let rec tclFIRST = function diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index c5d5c8c12..a3bc4707e 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -210,6 +210,7 @@ module New : sig val tclIFTHENELSE : unit tactic -> unit tactic -> unit tactic -> unit tactic val tclIFTHENSVELSE : unit tactic -> unit tactic array -> unit tactic -> unit tactic val tclIFTHENTRYELSEMUST : unit tactic -> unit tactic -> unit tactic + val tclIFTHENFIRSTTRYELSEMUST : unit tactic -> unit tactic -> unit tactic val tclDO : int -> unit tactic -> unit tactic val tclREPEAT : unit tactic -> unit tactic diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 29a30b4a2..7e281e2fe 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1190,7 +1190,7 @@ let onOpenInductionArg env sigma tac = function let sigma = Tacmach.New.project gl in tac clear_flag (sigma,(c,NoBindings)) end)) - | clear_flag,ElimOnIdent (_,id) -> + | clear_flag,ElimOnIdent {CAst.v=id} -> (* A quantified hypothesis *) Tacticals.New.tclTHEN (try_intros_until_id_check id) @@ -1206,7 +1206,7 @@ let onInductionArg tac = function Tacticals.New.tclTHEN (intros_until_n n) (Tacticals.New.onLastHyp (fun c -> tac clear_flag (c,NoBindings))) - | clear_flag,ElimOnIdent (_,id) -> + | clear_flag,ElimOnIdent {CAst.v=id} -> (* A quantified hypothesis *) Tacticals.New.tclTHEN (try_intros_until_id_check id) |