From 147afe827dc83602cc160a8b1357e84ecea910ff Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 5 Nov 2016 20:13:32 +0100
Subject: Evardefine API using EConstr.

---
 pretyping/pretype_errors.mli | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'pretyping/pretype_errors.mli')

diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli
index b015add799..8a6d8b6b37 100644
--- a/pretyping/pretype_errors.mli
+++ b/pretyping/pretype_errors.mli
@@ -45,14 +45,14 @@ type pretype_error =
   | CannotUnifyBindingType of constr * constr
   | CannotGeneralize of constr
   | NoOccurrenceFound of constr * Id.t option
-  | CannotFindWellTypedAbstraction of constr * constr list * (env * type_error) option
+  | CannotFindWellTypedAbstraction of constr * EConstr.constr list * (env * type_error) option
   | WrongAbstractionType of Name.t * constr * types * types
   | AbstractionOverMeta of Name.t * Name.t
   | NonLinearUnification of Name.t * constr
   (** Pretyping *)
   | VarNotFound of Id.t
   | UnexpectedType of constr * constr
-  | NotProduct of constr
+  | NotProduct of EConstr.constr
   | TypingError of type_error
   | CannotUnifyOccurrences of subterm_unification_error
   | UnsatisfiableConstraints of
@@ -110,7 +110,7 @@ val error_cannot_unify : ?loc:Loc.t -> env -> Evd.evar_map ->
 val error_cannot_unify_local : env -> Evd.evar_map -> constr * constr * constr -> 'b
 
 val error_cannot_find_well_typed_abstraction : env -> Evd.evar_map ->
-      constr -> constr list -> (env * type_error) option -> 'b
+      constr -> EConstr.constr list -> (env * type_error) option -> 'b
 
 val error_wrong_abstraction_type :  env -> Evd.evar_map ->
       Name.t -> constr -> types -> types -> 'b
@@ -132,7 +132,7 @@ val error_unexpected_type :
   ?loc:Loc.t -> env -> Evd.evar_map -> constr -> constr -> 'b
 
 val error_not_product :
-  ?loc:Loc.t -> env -> Evd.evar_map -> constr -> 'b
+  ?loc:Loc.t -> env -> Evd.evar_map -> EConstr.constr -> 'b
 
 (** {6 Error in conversion from AST to glob_constr } *)
 
-- 
cgit v1.2.3