diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-01-12 20:54:42 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-01-12 20:54:42 +0000 |
| commit | cb1830eaed49c8ac940fcfbd42fc8d4e3fd2a816 (patch) | |
| tree | c24a7272668ca2c60369209361ba5da596855584 /pretyping/pretype_errors.ml | |
| parent | e11a02fa93d68bc7e413d3218e0f7dc435b1936c (diff) | |
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
Diffstat (limited to 'pretyping/pretype_errors.ml')
| -rw-r--r-- | pretyping/pretype_errors.ml | 9 |
1 files changed, 7 insertions, 2 deletions
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml index b44dd94ef..2f7a7c87c 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 = |