diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/tacred.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 2768bb3fea..fbf9b34776 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -314,6 +314,7 @@ and construct_const env sigma = | None -> assert false | Some (c',rest) -> stacklam hnfstack [c'] c rest) + | IsLetIn (n,b,t,c) -> stacklam hnfstack [b] c stack | IsMutCase (ci,p,c,lf) -> hnfstack (special_red_case env (construct_const env sigma) (ci,p,c,lf), stack) |