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 /pretyping/locus.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 'pretyping/locus.ml')
| -rw-r--r-- | pretyping/locus.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/pretyping/locus.ml b/pretyping/locus.ml index 37dd120c1a..087a6b9174 100644 --- a/pretyping/locus.ml +++ b/pretyping/locus.ml @@ -20,6 +20,7 @@ type 'a or_var = type 'a occurrences_gen = | AllOccurrences + | AtLeastOneOccurrence | AllOccurrencesBut of 'a list (** non-empty *) | NoOccurrences | OnlyOccurrences of 'a list (** non-empty *) |