diff options
| author | Matthieu Sozeau | 2018-08-15 12:42:04 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2019-02-08 11:12:27 +0100 |
| commit | 781f050bcfabe02e225f3c1d29ee649610d6d680 (patch) | |
| tree | 05e55273b41c77879184ec32e29814d7b14fd863 /pretyping/evarconv.mli | |
| parent | dc8f191f2d81fd5f851b84e7aeda487df584197e (diff) | |
Abstraction naming
Diffstat (limited to 'pretyping/evarconv.mli')
| -rw-r--r-- | pretyping/evarconv.mli | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli index 994576c45b..c2ad4e6678 100644 --- a/pretyping/evarconv.mli +++ b/pretyping/evarconv.mli @@ -80,11 +80,10 @@ type occurrence_match_test = (** When given the choice of abstracting an occurrence or leaving it, force abstration. *) -type prefer_abstraction = bool type occurrence_selection = | AtOccurrences of occurrences - | Unspecified of prefer_abstraction + | Unspecified of Abstraction.abstraction (** By default, unspecified, not preferring abstraction. This provides the most general solutions. *) |