diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-12-18 09:32:07 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-12-18 09:32:07 +0000 |
| commit | 8bb6ef3137ce036fdb6f0f6b3debf4a7e4e30f09 (patch) | |
| tree | 56119be77961748b9489cc3a554d7052e8b518ed /pretyping/retyping.ml | |
| parent | 2c92d6fd70eb8752a732bb1f54cf64ef97ee444a (diff) | |
Grossière erreur de typage
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2305 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/retyping.ml')
| -rw-r--r-- | pretyping/retyping.ml | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index da12c6449..c2f42b34e 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -29,8 +29,7 @@ let rec subst_type env sigma typ = function | [] -> typ | h::rest -> match kind_of_term (whd_betadeltaiota env sigma typ) with - | Prod (na,c1,c2) -> - subst_type (push_rel (na,None,c1) env) sigma (subst1 h c2) rest + | Prod (na,c1,c2) -> subst_type env sigma (subst1 h c2) rest | _ -> anomaly "Non-functional construction" (* Si ft est le type d'un terme f, lequel est appliqué à args, *) |