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/unification.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/unification.ml')
| -rw-r--r-- | pretyping/unification.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/unification.ml b/pretyping/unification.ml index ac0b58b92b..ce97912b84 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -1649,7 +1649,7 @@ let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl = match occurrences_of_hyp hyp occs with | NoOccurrences, InHyp -> (push_named_context_val d sign,depdecls) - | AllOccurrences, InHyp as occ -> + | (AllOccurrences | AtLeastOneOccurrence), InHyp as occ -> let occ = if likefirst then LikeFirst else AtOccs occ in let newdecl = replace_term_occ_decl_modulo sigma occ test mkvarid d in if Context.Named.Declaration.equal (EConstr.eq_constr sigma) d newdecl |