From 3ef7797ef6fc605dfafb32523261fe1b023aeecb Mon Sep 17 00:00:00 2001
From: Samuel Mimram <smimram@debian.org>
Date: Fri, 28 Apr 2006 14:59:16 +0000
Subject: Imported Upstream version 8.0pl3+8.1alpha

---
 pretyping/pretype_errors.ml | 27 +++++++++++++++++++++++----
 1 file changed, 23 insertions(+), 4 deletions(-)

(limited to 'pretyping/pretype_errors.ml')

diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index fee1522f..48295c92 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: pretype_errors.ml,v 1.25.2.2 2004/07/16 19:30:45 herbelin Exp $ *)
+(* $Id: pretype_errors.ml 8688 2006-04-07 15:08:12Z msozeau $ *)
 
 open Util
 open Stdpp
@@ -24,8 +24,12 @@ type pretype_error =
   | CantFindCaseType of constr
   (* Unification *)
   | OccurCheck of existential_key * constr
-  | NotClean of existential_key * constr * hole_kind
-  | UnsolvableImplicit of hole_kind
+  | NotClean of existential_key * constr * Evd.hole_kind
+  | UnsolvableImplicit of Evd.hole_kind
+  | CannotUnify of constr * constr
+  | CannotUnifyBindingType of constr * constr
+  | CannotGeneralize of constr
+  | NoOccurrenceFound of constr
   (* Pretyping *)
   | VarNotFound of identifier
   | UnexpectedType of constr * constr
@@ -33,6 +37,12 @@ type pretype_error =
 
 exception PretypeError of env * pretype_error
 
+let precatchable_exception = function
+  | Util.UserError _ | TypeError _ | PretypeError _
+  | Stdpp.Exc_located(_,(Util.UserError _ | TypeError _ |
+    Nametab.GlobalizationError _ | PretypeError _)) -> true
+  | _ -> false
+
 let nf_evar = Reductionops.nf_evar
 let j_nf_evar sigma j = 
   { uj_val = nf_evar sigma j.uj_val;
@@ -43,7 +53,7 @@ let tj_nf_evar sigma {utj_val=v;utj_type=t} =
   {utj_val=type_app (nf_evar sigma) v;utj_type=t}
 
 let env_ise sigma env =
-  let sign = named_context env in
+  let sign = named_context_val env in
   let ctxt = rel_context env in
   let env0 = reset_with_named_context sign env in
   Sign.fold_rel_context
@@ -126,6 +136,9 @@ let error_ill_typed_rec_body_loc loc env sigma i na jl tys =
      IllTypedRecBody (i,na,jv_nf_evar sigma jl,
                       Array.map (nf_evar sigma) tys))
 
+let error_not_a_type_loc loc env sigma j =
+  raise_located_type_error (loc, env, sigma, NotAType (j_nf_evar sigma j))
+
 (*s Implicit arguments synthesis errors. It is hard to find
     a precise location. *)
 
@@ -141,6 +154,12 @@ let error_not_clean env sigma ev c (loc,k) =
 let error_unsolvable_implicit loc env sigma e =
   raise_with_loc loc (PretypeError (env_ise sigma env, UnsolvableImplicit e))
 
+let error_cannot_unify env sigma (m,n) =
+  raise (PretypeError (env_ise sigma env,CannotUnify (m,n)))
+
+let error_cannot_coerce env sigma (m,n) =
+  raise (PretypeError (env_ise sigma env,CannotUnify (m,n)))
+
 (*s Ml Case errors *)
 
 let error_cant_find_case_type_loc loc env sigma expr =
-- 
cgit v1.2.3