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 /engine/evd.ml | |
| parent | dc8f191f2d81fd5f851b84e7aeda487df584197e (diff) | |
Abstraction naming
Diffstat (limited to 'engine/evd.ml')
| -rw-r--r-- | engine/evd.ml | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/engine/evd.ml b/engine/evd.ml index 2d28892e6e..a89a67c287 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -128,11 +128,15 @@ end module Abstraction = struct - type t = bool list + type abstraction = + | Abstract + | Imitate + + type t = abstraction list let identity = [] - let abstract_last l = true :: l + let abstract_last l = Abstract :: l end (* The kinds of existential variables are now defined in [Evar_kinds] *) |