diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/equality.ml | 61 | ||||
| -rw-r--r-- | tactics/tacticals.ml | 1 | ||||
| -rw-r--r-- | tactics/tacticals.mli | 2 |
3 files changed, 34 insertions, 30 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml index 72a1267c3..b1f0360c4 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -119,36 +119,39 @@ let general_rewrite_bindings_in l2r id = let general_rewrite_in l2r id c = general_rewrite_bindings_clause (Some id) l2r (c,NoBindings) - let general_multi_rewrite l2r c cl = - let rec do_hyps = function - | [] -> tclIDTAC - | ((_,id),_) :: l -> - tclTHENFIRST (general_rewrite_bindings_in l2r id c) (do_hyps l) - in - let rec try_do_hyps = function - | [] -> tclIDTAC - | id :: l -> - tclTHENFIRST - (tclTRY (general_rewrite_bindings_in l2r id c)) - (try_do_hyps l) - in - if cl.concl_occs <> [] then - error "The \"at\" syntax isn't available yet for the rewrite/replace tactic" - else - tclTHENFIRST - (if cl.onconcl then general_rewrite_bindings l2r c else tclIDTAC) - (match cl.onhyps with - | Some l -> do_hyps l - | None -> - fun gl -> - (* try to rewrite in all hypothesis - (except maybe the rewritten one) *) - let ids = match kind_of_term (fst c) with - | Var id -> list_remove id (pf_ids_of_hyps gl) - | _ -> pf_ids_of_hyps gl - in try_do_hyps ids gl) - + if cl.concl_occs <> [] then + error "The \"at\" syntax isn't available yet for the rewrite/replace tactic" + else match cl.onhyps with + | Some l -> + (* If a precise list of locations is given, success is mandatory for + each of these locations. *) + let rec do_hyps = function + | [] -> tclIDTAC + | ((_,id),_) :: l -> + tclTHENFIRST (general_rewrite_bindings_in l2r id c) (do_hyps l) + in + if not cl.onconcl then do_hyps l + else tclTHENFIRST (general_rewrite_bindings l2r c) (do_hyps l) + | None -> + (* Otherwise, if we are told to rewrite in all hypothesis via the + syntax "* |-", we fail iff all the different rewrites fail *) + let rec do_hyps_atleastonce = function + | [] -> (fun gl -> error "Nothing to rewrite.") + | id :: l -> + tclIFTHENTRYELSEMUST + (general_rewrite_bindings_in l2r id c) + (do_hyps_atleastonce l) + in + let do_hyps gl = + (* If the term to rewrite is an hypothesis, don't rewrite in itself *) + let ids = match kind_of_term (fst c) with + | Var id -> list_remove id (pf_ids_of_hyps gl) + | _ -> pf_ids_of_hyps gl + in do_hyps_atleastonce ids gl + in + if not cl.onconcl then do_hyps + else tclIFTHENTRYELSEMUST (general_rewrite_bindings l2r c) do_hyps (* Conditional rewriting, the success of a rewriting is related to the resolution of the conditions by a given tactic *) diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index c5cf54d47..4aad135c6 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -68,6 +68,7 @@ let tclTHENTRY = tclTHENTRY let tclIFTHENELSE = tclIFTHENELSE let tclIFTHENSELSE = tclIFTHENSELSE let tclIFTHENSVELSE = tclIFTHENSVELSE +let tclIFTHENTRYELSEMUST = tclIFTHENTRYELSEMUST let unTAC = unTAC diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index 4b0e39e78..de6ce5964 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -64,7 +64,7 @@ val tclIFTHENELSE : tactic -> tactic -> tactic -> tactic val tclIFTHENSELSE : tactic -> tactic list -> tactic -> tactic val tclIFTHENSVELSE : tactic -> tactic array -> tactic -> tactic - +val tclIFTHENTRYELSEMUST : tactic -> tactic -> tactic val unTAC : tactic -> goal sigma -> proof_tree sigma |