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/tacred.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/tacred.ml')
| -rw-r--r-- | pretyping/tacred.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 2308a541fb..5db571433a 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -1105,6 +1105,7 @@ let unfoldoccs env sigma (occs,name) c = | AllOccurrences -> unfold env sigma name c | OnlyOccurrences l -> unfo true l | AllOccurrencesBut l -> unfo false l + | AtLeastOneOccurrence -> unfo false [] (* Unfold reduction tactic: *) let unfoldn loccname env sigma c = |