From cb1830eaed49c8ac940fcfbd42fc8d4e3fd2a816 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 12 Jan 2010 20:54:42 +0000
Subject: Removing some betaiota-redexes in error messages (an experiment)

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

(limited to 'pretyping/pretype_errors.ml')

diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index b44dd94ef6..2f7a7c87cc 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -51,7 +51,12 @@ let nf_evar = Reductionops.nf_evar
 let j_nf_evar sigma j =
   { uj_val = nf_evar sigma j.uj_val;
     uj_type = nf_evar sigma j.uj_type }
+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_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}
@@ -112,11 +117,11 @@ let error_cant_apply_not_functional_loc loc env sigma rator randl =
     CantApplyNonFunctional (j_nf_evar sigma rator, ja))
 
 let error_cant_apply_bad_type_loc loc env sigma (n,c,t) rator randl =
-  let ja = Array.of_list (jl_nf_evar sigma randl) in
+  let ja = Array.of_list (jl_nf_betaiotaevar sigma randl) in
   raise_located_type_error
     (loc, env, sigma,
      CantApplyBadType
-       ((n,nf_evar sigma c, nf_evar sigma t),
+       ((n,nf_evar sigma c, Reductionops.nf_betaiota sigma t),
         j_nf_evar sigma rator, ja))
 
 let error_ill_formed_branch_loc loc env sigma c i actty expty =
-- 
cgit v1.2.3