aboutsummaryrefslogtreecommitdiff
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/evarutil.ml1
1 files changed, 0 insertions, 1 deletions
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 4ccf4817cd..a53ecf5355 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -71,7 +71,6 @@ let whd_castappevar_stack sigma c =
whrec (existential_value sigma (ev,args), l)
| Cast (c,_) -> whrec (c, l)
| App (f,args) -> whrec (f, Array.fold_right (fun a l -> a::l) args l)
- | LetIn (_,v,_,b) -> whrec (subst1 v b, l)
| _ -> s
in
whrec (c, [])