From c31fabdc5aadbf22d1d27f22aa737188acc6f12b Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 27 Aug 2007 11:41:08 +0000
Subject: Suppression des type_app et body_of_type qui alourdissent inutilement
 le code

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

(limited to 'pretyping/pretype_errors.ml')

diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index 4a0f12d66c..26ccc8024b 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -51,7 +51,7 @@ let j_nf_evar sigma j =
 let jl_nf_evar sigma jl = List.map (j_nf_evar 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=type_app (nf_evar sigma) 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
-- 
cgit v1.2.3