From 3a0b543af4ac99b29efdebe27b1d204d044a7bf0 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Sat, 31 Mar 2018 17:43:18 +0200
Subject: Evar maps contain econstrs.

We bootstrap the circular evar_map <-> econstr dependency by moving
the internal EConstr.API module to Evd.MiniEConstr. Then we make the
Evd functions use econstr.
---
 engine/eConstr.mli | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

(limited to 'engine/eConstr.mli')

diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index 9cc9bf680c..9a5b5ec3a3 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -13,7 +13,7 @@ open Names
 open Constr
 open Environ
 
-type t
+type t = Evd.econstr
 (** Type of incomplete terms. Essentially a wrapper around {!Constr.t} ensuring
     that {!Constr.kind} does not observe defined evars. *)
 
@@ -290,6 +290,7 @@ val is_global : Evd.evar_map -> Globnames.global_reference -> t -> bool
 
 (** {5 Extra} *)
 
+val of_existential : Constr.existential -> existential
 val of_named_decl : (Constr.t, Constr.types) Context.Named.Declaration.pt -> (t, types) Context.Named.Declaration.pt
 val of_rel_decl : (Constr.t, Constr.types) Context.Rel.Declaration.pt -> (t, types) Context.Rel.Declaration.pt
 
@@ -308,6 +309,8 @@ sig
   val to_named_decl : (t, types) Context.Named.Declaration.pt -> (Constr.t, Constr.types) Context.Named.Declaration.pt
   (** Physical identity. Does not care for defined evars. *)
 
+  val to_named_context : (t, types) Context.Named.pt -> Context.Named.t
+
   val to_sorts : ESorts.t -> Sorts.t
   (** Physical identity. Does not care for normalization. *)
 
-- 
cgit v1.2.3