From 85fb5f33b1cac28e1fe4f00741c66f6f58109f84 Mon Sep 17 00:00:00 2001
From: barras
Date: Fri, 3 Sep 2004 17:14:02 +0000
Subject: premiere reorganisation de l\'unification

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6057 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/pretype_errors.mli | 7 +++++++
 1 file changed, 7 insertions(+)

(limited to 'pretyping/pretype_errors.mli')

diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli
index e09a6d1d10..2f9b1dc46a 100644
--- a/pretyping/pretype_errors.mli
+++ b/pretyping/pretype_errors.mli
@@ -28,6 +28,9 @@ type pretype_error =
   | OccurCheck of existential_key * constr
   | NotClean of existential_key * constr * hole_kind
   | UnsolvableImplicit of hole_kind
+  | CannotUnify of constr * constr
+  | CannotGeneralize of constr
+  | NoOccurrenceFound of constr
   (* Pretyping *)
   | VarNotFound of identifier
   | UnexpectedType of constr * constr
@@ -35,6 +38,8 @@ type pretype_error =
 
 exception PretypeError of env * pretype_error
 
+val precatchable_exception : exn -> bool
+
 (* Presenting terms without solved evars *)
 val nf_evar :  Evd.evar_map -> constr -> constr
 val j_nf_evar :  Evd.evar_map -> unsafe_judgment -> unsafe_judgment
@@ -82,6 +87,8 @@ val error_not_clean :
 
 val error_unsolvable_implicit : loc -> env -> Evd.evar_map -> hole_kind -> 'b
 
+val error_cannot_unify : env -> Evd.evar_map -> constr * constr -> 'b
+
 (*s Ml Case errors *)
 
 val error_cant_find_case_type_loc :
-- 
cgit v1.2.3