From 7b43de20a4acd7c9da290f038d9a16fe67eccd59 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 19 Nov 2016 01:59:07 +0100
Subject: Leminv API using EConstr.

---
 engine/evarutil.mli | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'engine/evarutil.mli')

diff --git a/engine/evarutil.mli b/engine/evarutil.mli
index 82346b24e2..ad3851ea31 100644
--- a/engine/evarutil.mli
+++ b/engine/evarutil.mli
@@ -170,7 +170,7 @@ val nf_evar_map_universes : evar_map -> evar_map * (constr -> constr)
 
 (** Replacing all evars, possibly raising [Uninstantiated_evar] *)
 exception Uninstantiated_evar of existential_key
-val flush_and_check_evars :  evar_map -> constr -> constr
+val flush_and_check_evars :  evar_map -> EConstr.constr -> constr
 
 (** {6 Term manipulation up to instantiation} *)
 
@@ -220,7 +220,7 @@ val push_rel_decl_to_named_context :
 val push_rel_context_to_named_context : Environ.env -> EConstr.types ->
   named_context_val * EConstr.types * EConstr.constr list * csubst * (identifier*EConstr.constr) list
 
-val generalize_evar_over_rels : evar_map -> existential -> types * constr list
+val generalize_evar_over_rels : evar_map -> EConstr.existential -> EConstr.types * EConstr.constr list
 
 (** Evar combinators *)
 
-- 
cgit v1.2.3