From 7799626c67c39c6bd2c5faf247456efb2c26ae82 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Tue, 12 Dec 2017 04:34:45 +0100
Subject: [econstr] Cleanup in `vernac/classes.ml`.

We fix quite a few types, and perform some cleanup wrt to the
evar_map, in particular we prefer to thread it now as otherwise
it may become trickier to check when we are using the correct one.

Thanks to @SkySkimmer for lots of comments and bug-finding.
---
 engine/eConstr.ml  | 2 ++
 engine/eConstr.mli | 2 ++
 2 files changed, 4 insertions(+)

(limited to 'engine')

diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index d303038c5d..53123c9334 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -150,6 +150,8 @@ type rel_declaration = (constr, types) Context.Rel.Declaration.pt
 type named_context = (constr, types) Context.Named.pt
 type rel_context = (constr, types) Context.Rel.pt
 
+type 'a puniverses = 'a * EInstance.t
+
 let in_punivs a = (a, EInstance.empty)
 
 let mkProp = of_kind (Sort (ESorts.make Sorts.prop))
diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index f54c422adc..6f2a30f4a3 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -56,6 +56,8 @@ sig
   val is_empty : t -> bool
 end
 
+type 'a puniverses = 'a * EInstance.t
+
 (** {5 Destructors} *)
 
 val kind : Evd.evar_map -> t -> (t, t, ESorts.t, EInstance.t) Constr.kind_of_term
-- 
cgit v1.2.3