From 5da9926d98d05cd34cd9b6496b0598bcb7184d94 Mon Sep 17 00:00:00 2001
From: mohring
Date: Wed, 26 Jun 2002 14:30:13 +0000
Subject: *** empty log message ***

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

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 2360de8244..fe6b170181 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -329,7 +329,8 @@ let rec pretype tycon env isevars lvar lmeta = function
       let j' = pretype tycon (push_rel var env) isevars lvar lmeta c2 in
       { uj_val = mkLetIn (name, j.uj_val, t, j'.uj_val) ;
 	uj_type = type_app (subst1 j.uj_val) j'.uj_type }
-      
+
+(* Special Case for let constructions to avoid exponential behavior *)      
   | ROldCase (loc,false,po,c,[| f |]) ->
       let cj = pretype empty_tycon env isevars lvar lmeta c in
       let (IndType (indf,realargs) as indt) = 
-- 
cgit v1.2.3