diff options
| author | letouzey | 2007-07-06 16:35:07 +0000 |
|---|---|---|
| committer | letouzey | 2007-07-06 16:35:07 +0000 |
| commit | 9dec278bb1af17f30021bf0bb04f21682d1f0a3c (patch) | |
| tree | 28bdb13371312f336f37634c9cc6ef6740bea637 /tactics/equality.ml | |
| parent | 4d75ddfdc0382e0d6e163febe12912fe477aa43b (diff) | |
Adding a syntax for "n-ary" rewrite:
rewrite H, H'
means: rewrite H; rewrite H'.
This should still be compatible with other "features" of rewrite: like
orientation, implicit arguments (t:=...), and "in" clause. Concerning
the "in" clause, for the moment only one is allowed at the very end of
the tactic, and it applies to all the different rewrites that are
done. For instance, if someone _really_ wants to use all features at
the same time:
rewrite H1 with (t:=u), <-H2, H3 in *
means: rewrite H1 with (t:=u) in *; rewrite <- H2 in *; rewrite H3 in *
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9954 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/equality.ml')
| -rw-r--r-- | tactics/equality.ml | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml index c5b7aeedfb..4f94ba5953 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -166,6 +166,12 @@ let general_multi_rewrite l2r with_evars c cl = (general_rewrite_ebindings l2r c with_evars) do_hyps +let rec general_multi_multi_rewrite with_evars l cl = match l with + | [] -> tclIDTAC + | (l2r,c)::l -> + tclTHEN (general_multi_rewrite l2r with_evars c cl) + (general_multi_multi_rewrite with_evars l cl) + (* Conditional rewriting, the success of a rewriting is related to the resolution of the conditions by a given tactic *) |