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 /plugins | |
| 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 'plugins')
| -rw-r--r-- | plugins/ltac/tacintern.ml | 2 | ||||
| -rw-r--r-- | plugins/ltac/tacinterp.ml | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml index a1e21aab04..543d4de0fe 100644 --- a/plugins/ltac/tacintern.ml +++ b/plugins/ltac/tacintern.ml @@ -557,7 +557,7 @@ let rec intern_atomic lf ist x = | _ -> false in let is_onconcl = match cl.concl_occs with - | AllOccurrences | NoOccurrences -> true + | AtLeastOneOccurrence | AllOccurrences | NoOccurrences -> true | _ -> false in TacChange (None, diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 525ff7fd0f..d17a8e3cc8 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -1746,7 +1746,7 @@ and interp_atomic ist tac : unit Proofview.tactic = | _ -> false in let is_onconcl = match cl.concl_occs with - | AllOccurrences | NoOccurrences -> true + | AtLeastOneOccurrence | AllOccurrences | NoOccurrences -> true | _ -> false in let c_interp patvars env sigma = |