diff options
| author | Matthieu Sozeau | 2017-07-28 15:31:28 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2019-02-08 10:55:51 +0100 |
| commit | c039d78bd098a499a34038e64bd1e5fbe280d7f3 (patch) | |
| tree | 8bcc7cd765321a9df77c3888bd3d3a28a35438f2 /tactics/ppred.ml | |
| parent | 46b671c7473385ec7747a796e85b3cf704d000c6 (diff) | |
locus: Add an AtLeastOneOccurrence constructor.
The semantics is obviously that it is an error if not at least one
occurrence is found (natural semantics for rewriting for
example).
Diffstat (limited to 'tactics/ppred.ml')
| -rw-r--r-- | tactics/ppred.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/tactics/ppred.ml b/tactics/ppred.ml index dd1bcd4699..d832dc279c 100644 --- a/tactics/ppred.ml +++ b/tactics/ppred.ml @@ -6,6 +6,7 @@ open Pputils let pr_with_occurrences pr keyword (occs,c) = match occs with + | AtLeastOneOccurrence -> hov 1 (pr c ++ spc () ++ keyword "at" ++ str" +") | AllOccurrences -> pr c | NoOccurrences -> |