diff options
| author | mohring | 2002-06-26 14:30:13 +0000 |
|---|---|---|
| committer | mohring | 2002-06-26 14:30:13 +0000 |
| commit | 5da9926d98d05cd34cd9b6496b0598bcb7184d94 (patch) | |
| tree | 918e773ef56049918837100217780654ebe5e655 | |
| parent | b3bf7247cae6ed54d60c012052e0fb51dc1984b7 (diff) | |
*** empty log message ***
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2809 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | pretyping/pretyping.ml | 3 |
1 files changed, 2 insertions, 1 deletions
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) = |