Merge PR #6392: [econstr] Cleanup in `vernac/classes.ml`

2 files changed, 4 insertions, 0 deletions

diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index d303038c5..53123c933 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 f54c422ad..6f2a30f4a 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