diff options
| author | herbelin | 2013-03-21 19:12:58 +0000 |
|---|---|---|
| committer | herbelin | 2013-03-21 19:12:58 +0000 |
| commit | f687552465f86bfd66ada997a26486b2a20d5363 (patch) | |
| tree | 026113c71989f20ec0073a72ffad606868d2de94 /pretyping | |
| parent | b069aa8d6db23269f0c4f250f271411c2a26fcda (diff) | |
Fixing an old pecularity of "red": head betaiota redexes are now
reduced in order to find some head constant to reduce.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16337 85f007b7-540e-0410-9357-904b9bb8a0f7
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 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 |