From 781f050bcfabe02e225f3c1d29ee649610d6d680 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 15 Aug 2018 12:42:04 +0200
Subject: Abstraction naming

---
 engine/evd.ml  | 8 ++++++--
 engine/evd.mli | 6 +++++-
 2 files changed, 11 insertions(+), 3 deletions(-)

(limited to 'engine')

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
 
-- 
cgit v1.2.3