diff options
Diffstat (limited to 'pretyping')
| -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, *) |