diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-07-21 13:43:31 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-03-01 12:05:39 +0100 |
| commit | 711b9d8cdf6e25690d247d9e8c49f005527e64e2 (patch) | |
| tree | 5a19ec52e7a510a456195d3814958abc33e47f73 /tactics/tacticals.mli | |
| parent | f726e860917b56abc94f21d9d5add7594d23bb6d (diff) | |
Fixing rewriting in side conditions for "rewrite in *" and "rewrite in * |-".
Noticed by Sigurd Schneider.
Diffstat (limited to 'tactics/tacticals.mli')
| -rw-r--r-- | tactics/tacticals.mli | 1 |
1 files changed, 1 insertions, 0 deletions
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 |