diff options
| author | msozeau | 2008-03-07 16:32:12 +0000 |
|---|---|---|
| committer | msozeau | 2008-03-07 16:32:12 +0000 |
| commit | ec850ff623801e514b3ed0a42beb6f7984992520 (patch) | |
| tree | 6a03dd3d0545b927326f28e7d8da08a850cead5f /tactics/equality.mli | |
| parent | 905c47d6a07cc69b9e7aa0b9d73caeacf2b1d2be (diff) | |
Fix bug #1704 (ordering of condition goals for (setoid)rewrite). As part
of the fix I added an optional "by" annotation for rewrite to solve said
conditions in the same tactic call. Most of the theories have been
updated, only FSets is missing, Pierre will take care of it.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10634 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/equality.mli')
| -rw-r--r-- | tactics/equality.mli | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/tactics/equality.mli b/tactics/equality.mli index 846487f964..91a0d33c6d 100644 --- a/tactics/equality.mli +++ b/tactics/equality.mli @@ -53,7 +53,8 @@ val general_rewrite_in : val general_multi_rewrite : bool -> evars_flag -> constr with_ebindings -> clause -> tactic val general_multi_multi_rewrite : - evars_flag -> (bool * multi * constr with_ebindings) list -> clause -> tactic + evars_flag -> (bool * multi * constr with_ebindings) list -> clause -> + tactic option -> tactic val conditional_rewrite : bool -> tactic -> constr with_ebindings -> tactic val conditional_rewrite_in : |