Imported Upstream version 8.4~betaupstream/8.4_beta

1 files changed, 45 insertions, 68 deletions

diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index 688a25b9..2cf16791 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -1,15 +1,13 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: pretype_errors.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
-
+open Compat
 open Util
-open Stdpp
 open Names
 open Sign
 open Term
@@ -17,7 +15,7 @@ open Termops
 open Namegen
 open Environ
 open Type_errors
-open Rawterm
+open Glob_term
 open Inductiveops
 
 type pretype_error =
@@ -40,12 +38,13 @@ type pretype_error =
   | VarNotFound of identifier
   | UnexpectedType of constr * constr
   | NotProduct of constr
+  | TypingError of type_error
 
-exception PretypeError of env * pretype_error
+exception PretypeError of env * Evd.evar_map * pretype_error
 
 let precatchable_exception = function
   | Util.UserError _ | TypeError _ | PretypeError _
-  | Stdpp.Exc_located(_,(Util.UserError _ | TypeError _ |
+  | Loc.Exc_located(_,(Util.UserError _ | TypeError _ |
     Nametab.GlobalizationError _ | PretypeError _)) -> true
   | _ -> false
 
@@ -57,25 +56,22 @@ let j_nf_betaiotaevar sigma j =
   { uj_val = nf_evar sigma j.uj_val;
     uj_type = Reductionops.nf_betaiota sigma j.uj_type }
 let jl_nf_evar sigma jl = List.map (j_nf_evar sigma) jl
-let jl_nf_betaiotaevar sigma jl =
-  List.map (j_nf_betaiotaevar sigma) jl
+let jv_nf_betaiotaevar sigma jl =
+  Array.map (j_nf_betaiotaevar sigma) jl
 let jv_nf_evar sigma = Array.map (j_nf_evar sigma)
 let tj_nf_evar sigma {utj_val=v;utj_type=t} =
   {utj_val=nf_evar sigma v;utj_type=t}
 
-let env_ise sigma env =
-  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
-    (fun (na,b,ty) e ->
-      push_rel
-        (na, Option.map (nf_evar sigma) b, nf_evar sigma ty)
-        e)
-    ctxt
-    ~init:env0
-
-(* This simplify the typing context of Cases clauses *)
+let env_nf_evar sigma env =
+  process_rel_context
+    (fun d e -> push_rel (map_rel_declaration (nf_evar sigma) d) e) env
+
+let env_nf_betaiotaevar sigma env =
+  process_rel_context
+    (fun d e ->
+      push_rel (map_rel_declaration (Reductionops.nf_betaiota sigma) d) e) env
+
+(* This simplifies the typing context of Cases clauses *)
 (* hope it does not disturb other typing contexts *)
 let contract env lc =
   let l = ref [] in
@@ -99,111 +95,92 @@ let contract2 env a b = match contract env [a;b] with
 let contract3 env a b c = match contract env [a;b;c] with
   | env, [a;b;c] -> env,a,b,c | _ -> assert false
 
-let raise_pretype_error (loc,ctx,sigma,te) =
-  Stdpp.raise_with_loc loc (PretypeError(env_ise sigma ctx,te))
+let raise_pretype_error (loc,env,sigma,te) =
+  Loc.raise loc (PretypeError(env,sigma,te))
 
-let raise_located_type_error (loc,ctx,sigma,te) =
-  Stdpp.raise_with_loc loc (TypeError(env_ise sigma ctx,te))
+let raise_located_type_error (loc,env,sigma,te) =
+  Loc.raise loc (PretypeError(env,sigma,TypingError te))
 
 
 let error_actual_type_loc loc env sigma {uj_val=c;uj_type=actty} expty =
   let env, c, actty, expty = contract3 env c actty expty in
-  let j = j_nf_evar sigma {uj_val=c;uj_type=actty} in
-  raise_located_type_error
-    (loc, env, sigma, ActualType (j, nf_evar sigma expty))
+  let j = {uj_val=c;uj_type=actty} in
+  raise_located_type_error (loc, env, sigma, ActualType (j, expty))
 
 let error_cant_apply_not_functional_loc loc env sigma rator randl =
-  let ja = Array.of_list (jl_nf_evar sigma randl) in
   raise_located_type_error
-    (loc, env, sigma,
-    CantApplyNonFunctional (j_nf_evar sigma rator, ja))
+    (loc, env, sigma, CantApplyNonFunctional (rator, Array.of_list randl))
 
 let error_cant_apply_bad_type_loc loc env sigma (n,c,t) rator randl =
-  let ja = Array.of_list (jl_nf_betaiotaevar sigma randl) in
   raise_located_type_error
     (loc, env, sigma,
-     CantApplyBadType
-       ((n,nf_evar sigma c, Reductionops.nf_betaiota sigma t),
-        j_nf_evar sigma rator, ja))
+       CantApplyBadType ((n,c,t), rator, Array.of_list randl))
 
 let error_ill_formed_branch_loc loc env sigma c i actty expty =
-  let simp t = Reduction.nf_betaiota (nf_evar sigma t) in
   raise_located_type_error
-    (loc, env, sigma,
-     IllFormedBranch (nf_evar sigma c,i,simp actty, simp expty))
+    (loc, env, sigma, IllFormedBranch (c, i, actty, expty))
 
 let error_number_branches_loc loc env sigma cj expn =
-  raise_located_type_error
-    (loc, env, sigma,
-     NumberBranches (j_nf_evar sigma cj, expn))
+  raise_located_type_error (loc, env, sigma, NumberBranches (cj, expn))
 
 let error_case_not_inductive_loc loc env sigma cj =
-  raise_located_type_error
-    (loc, env, sigma, CaseNotInductive (j_nf_evar sigma cj))
+  raise_located_type_error (loc, env, sigma, CaseNotInductive cj)
 
 let error_ill_typed_rec_body_loc loc env sigma i na jl tys =
   raise_located_type_error
-    (loc, env, sigma,
-     IllTypedRecBody (i,na,jv_nf_evar sigma jl,
-                      Array.map (nf_evar sigma) tys))
+    (loc, env, sigma, IllTypedRecBody (i, na, jl, tys))
 
 let error_not_a_type_loc loc env sigma j =
-  raise_located_type_error (loc, env, sigma, NotAType (j_nf_evar sigma j))
+  raise_located_type_error (loc, env, sigma, NotAType j)
 
 (*s Implicit arguments synthesis errors. It is hard to find
     a precise location. *)
 
 let error_occur_check env sigma ev c =
-  let c = nf_evar sigma c in
-  raise (PretypeError (env_ise sigma env, OccurCheck (ev,c)))
+  raise (PretypeError (env, sigma, OccurCheck (ev,c)))
 
 let error_not_clean env sigma ev c (loc,k) =
-  let c = nf_evar sigma c in
-  raise_with_loc loc
-    (PretypeError (env_ise sigma env,  NotClean (ev,c,k)))
+  Loc.raise loc (PretypeError (env, sigma, NotClean (ev,c,k)))
 
 let error_unsolvable_implicit loc env sigma evi e explain =
-  raise_with_loc loc
-    (PretypeError (env_ise sigma env, UnsolvableImplicit (evi, e, explain)))
+  Loc.raise loc
+    (PretypeError (env, sigma, UnsolvableImplicit (evi, e, explain)))
 
 let error_cannot_unify env sigma (m,n) =
-  raise (PretypeError (env_ise sigma env,CannotUnify (m,n)))
+  raise (PretypeError (env, sigma,CannotUnify (m,n)))
 
 let error_cannot_unify_local env sigma (m,n,sn) =
-  raise (PretypeError (env_ise sigma env,CannotUnifyLocal (m,n,sn)))
+  raise (PretypeError (env, sigma,CannotUnifyLocal (m,n,sn)))
 
 let error_cannot_coerce env sigma (m,n) =
-  raise (PretypeError (env_ise sigma env,CannotUnify (m,n)))
+  raise (PretypeError (env, sigma,CannotUnify (m,n)))
 
 let error_cannot_find_well_typed_abstraction env sigma p l =
-  raise (PretypeError (env_ise sigma env,CannotFindWellTypedAbstraction (p,l)))
+  raise (PretypeError (env, sigma,CannotFindWellTypedAbstraction (p,l)))
 
 let error_abstraction_over_meta env sigma hdmeta metaarg =
   let m = Evd.meta_name sigma hdmeta and n = Evd.meta_name sigma metaarg in
-  raise (PretypeError (env_ise sigma env,AbstractionOverMeta (m,n)))
+  raise (PretypeError (env, sigma,AbstractionOverMeta (m,n)))
 
 let error_non_linear_unification env sigma hdmeta t =
   let m = Evd.meta_name sigma hdmeta in
-  raise (PretypeError (env_ise sigma env,NonLinearUnification (m,t)))
+  raise (PretypeError (env, sigma,NonLinearUnification (m,t)))
 
 (*s Ml Case errors *)
 
 let error_cant_find_case_type_loc loc env sigma expr =
-  raise_pretype_error
-    (loc, env, sigma, CantFindCaseType (nf_evar sigma expr))
+  raise_pretype_error (loc, env, sigma, CantFindCaseType expr)
 
 (*s Pretyping errors *)
 
 let error_unexpected_type_loc loc env sigma actty expty =
   let env, actty, expty = contract2 env actty expty in
-  raise_pretype_error
-    (loc, env, sigma,
-     UnexpectedType (nf_evar sigma actty, nf_evar sigma expty))
+  raise_pretype_error (loc, env, sigma, UnexpectedType (actty, expty))
 
 let error_not_product_loc loc env sigma c =
-  raise_pretype_error (loc, env, sigma, NotProduct (nf_evar sigma c))
+  raise_pretype_error (loc, env, sigma, NotProduct c)
 
-(*s Error in conversion from AST to rawterms *)
+(*s Error in conversion from AST to glob_constr *)
 
 let error_var_not_found_loc loc s =
   raise_pretype_error (loc, empty_env, Evd.empty, VarNotFound s)