diff options
Diffstat (limited to 'pretyping/tacred.ml')
| -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 47c382c2e6..86195edd22 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -783,6 +783,7 @@ and whd_construct_stack env sigma s = let try_red_product env sigma c = let simpfun = clos_norm_flags betaiotazeta env sigma in let rec redrec env x = + let x = whd_betaiota sigma x in match kind_of_term x with | App (f,l) -> (match kind_of_term f with |