A few more betaiota on environments and types of error messages. Seems to

be convenient in general.

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

3 files changed, 13 insertions, 13 deletions

diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index c0fa620485..6d1c54e63d 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -63,16 +63,13 @@ let tj_nf_evar sigma {utj_val=v;utj_type=t} =
   {utj_val=nf_evar sigma v;utj_type=t}
 
 let env_nf_evar 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
+  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 simplify the typing context of Cases clauses *)
 (* hope it does not disturb other typing contexts *)
diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli
index b558020440..30ee6aaf67 100644
--- a/pretyping/pretype_errors.mli
+++ b/pretyping/pretype_errors.mli
@@ -51,6 +51,9 @@ val jv_nf_evar : Evd.evar_map -> unsafe_judgment array -> unsafe_judgment array
 val tj_nf_evar : Evd.evar_map -> unsafe_type_judgment -> unsafe_type_judgment
 
 val env_nf_evar : Evd.evar_map -> env -> env
+val env_nf_betaiotaevar : Evd.evar_map -> env -> env
+
+val j_nf_betaiotaevar : Evd.evar_map -> unsafe_judgment -> unsafe_judgment
 val jv_nf_betaiotaevar :
   Evd.evar_map -> unsafe_judgment array -> unsafe_judgment array
 
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 1c677de95c..9443217f1b 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -154,8 +154,8 @@ let explain_generalization env (name,var) j =
   spc () ++ str "which should be Set, Prop or Type."
 
 let explain_actual_type env sigma j pt =
-  let j = j_nf_evar sigma j in
-  let pt = nf_evar sigma pt in
+  let j = j_nf_betaiotaevar sigma j in
+  let pt = nf_betaiota sigma pt in
   let pe = pr_ne_context_of (str "In environment") env in
   let (pc,pct) = pr_ljudge_env env j in
   let pt = pr_lconstr_env env pt in
@@ -507,7 +507,7 @@ let explain_type_error env sigma err =
       explain_wrong_case_info env ind ci
 
 let explain_pretype_error env sigma err =
-  let env = env_nf_evar sigma env in
+  let env = env_nf_betaiotaevar sigma env in
   let env = make_all_name_different env in
   match err with
   | CantFindCaseType c -> explain_cant_find_case_type env sigma c