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 ++
 1 file changed, 2 insertions(+)

(limited to 'engine/eConstr.ml')

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