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 /_CoqProject | |
| 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 '_CoqProject')
0 files changed, 0 insertions, 0 deletions