Passage à des contextes de vars et de rels pouvant contenir des déclarations

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@568 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 20 insertions, 22 deletions

diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml
index d2891180a..14409c235 100644
--- a/kernel/type_errors.ml
+++ b/kernel/type_errors.ml
@@ -40,61 +40,59 @@ type type_error =
   | WrongPredicateArity of constr * int * int
   | NeedsInversion of constr * constr
 
-exception TypeError of path_kind * context * type_error
+exception TypeError of path_kind * env * type_error
 
-let context_ise sigma env =
-  map_var_env (typed_app (Reduction.nf_ise1 sigma))
-    (map_rel_env (typed_app (Reduction.nf_ise1 sigma))
-       (context env))
+let env_ise sigma env =
+  map_context (Reduction.nf_ise1 sigma) env
 
 let error_unbound_rel k env sigma n =
-  raise (TypeError (k, context_ise sigma env, UnboundRel n))
+  raise (TypeError (k, env_ise sigma env, UnboundRel n))
 
 let error_not_type k env c =
-  raise (TypeError (k, context env, NotAType c))
+  raise (TypeError (k, env, NotAType c))
 
 let error_assumption k env c =
-  raise (TypeError (k, context env, BadAssumption c))
+  raise (TypeError (k, env, BadAssumption c))
 
 let error_reference_variables k env id =
-  raise (TypeError (k, context env, ReferenceVariables id))
+  raise (TypeError (k, env, ReferenceVariables id))
 
 let error_elim_arity k env ind aritylst c p pt okinds = 
-  raise (TypeError (k, context env, ElimArity (ind,aritylst,c,p,pt,okinds)))
+  raise (TypeError (k, env, ElimArity (ind,aritylst,c,p,pt,okinds)))
 
 let error_case_not_inductive k env c ct = 
-  raise (TypeError (k, context env, CaseNotInductive (c,ct)))
+  raise (TypeError (k, env, CaseNotInductive (c,ct)))
 
 let error_number_branches k env c ct expn =
-  raise (TypeError (k, context env, NumberBranches (c,ct,expn)))
+  raise (TypeError (k, env, NumberBranches (c,ct,expn)))
 
 let error_ill_formed_branch k env c i actty expty =
-  raise (TypeError (k, context env, IllFormedBranch (c,i,actty,expty)))
+  raise (TypeError (k, env, IllFormedBranch (c,i,actty,expty)))
 
 let error_generalization k env sigma nvar c =
-  raise (TypeError (k, context_ise sigma env, Generalization (nvar,c)))
+  raise (TypeError (k, env_ise sigma env, Generalization (nvar,c)))
 
 let error_actual_type k env c actty expty =
-  raise (TypeError (k, context env, ActualType (c,actty,expty)))
+  raise (TypeError (k, env, ActualType (c,actty,expty)))
 
 let error_cant_apply_not_functional k env rator randl =
-  raise (TypeError (k, context env, CantApplyNonFunctional (rator,randl)))
+  raise (TypeError (k, env, CantApplyNonFunctional (rator,randl)))
 
 let error_cant_apply_bad_type k env sigma t rator randl =
-  raise(TypeError (k, context_ise sigma env, CantApplyBadType (t,rator,randl)))
+  raise(TypeError (k, env_ise sigma env, CantApplyBadType (t,rator,randl)))
 
 let error_ill_formed_rec_body k env str lna i vdefs =
-  raise (TypeError (k, context env, IllFormedRecBody (str,lna,i,vdefs)))
+  raise (TypeError (k, env, IllFormedRecBody (str,lna,i,vdefs)))
 
 let error_ill_typed_rec_body k env i lna vdefj vargs =
-  raise (TypeError (k, context env, IllTypedRecBody (i,lna,vdefj,vargs)))
+  raise (TypeError (k, env, IllTypedRecBody (i,lna,vdefj,vargs)))
 
 let error_not_inductive k env c =
-  raise (TypeError (k, context env, NotInductive c))
+  raise (TypeError (k, env, NotInductive c))
 
 let error_ml_case k env mes c ct br brt =
-  raise (TypeError (k, context env, MLCase (mes,c,ct,br,brt)))
+  raise (TypeError (k, env, MLCase (mes,c,ct,br,brt)))
 
 let error_not_product env c =
-  raise (TypeError (CCI, context env, NotProduct c))
+  raise (TypeError (CCI, env, NotProduct c))