diff options
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/evd.ml | 8 | ||||
| -rw-r--r-- | engine/evd.mli | 6 |
2 files changed, 11 insertions, 3 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] *) diff --git a/engine/evd.mli b/engine/evd.mli index 1f6a0da882..fcccb1be5a 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -78,7 +78,11 @@ sig end module Abstraction : sig - type t = bool list + type abstraction = + | Abstract + | Imitate + + type t = abstraction list val identity : t |