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 | |
| 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
| -rw-r--r-- | CHANGES | 2 | ||||
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 4 | ||||
| -rw-r--r-- | pretyping/tacred.ml | 1 | ||||
| -rw-r--r-- | tactics/tactics.ml | 4 |
4 files changed, 10 insertions, 1 deletions
@@ -30,6 +30,8 @@ Tactics - Similarly, "intuition" has been made more uniform and, where it now fails, "dintuition" can be used. (possible source of incompatibilities) - Tactic notations can now be defined locally to a module (use "Local" prefix). +- Tactic "red" now reduces head beta-iota redexes (potential source of + rare incompatibilities). Program diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index d59e62640e..a2d02a4ca8 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -2899,7 +2899,9 @@ computational expressions (i.e. with few dead code). \tacindex{red} This tactic applies to a goal that has the form {\tt - forall (x:T1)\dots(xk:Tk), c t1 \dots\ tn} where {\tt c} is a constant. If + forall (x:T1)\dots(xk:Tk), t} with {\tt t} +$\beta\iota\zeta$-reducing to {\tt c t1 \dots\ tn} and {\tt c} a +constant. If {\tt c} is transparent then it replaces {\tt c} with its definition (say {\tt t}) and then reduces {\tt (t t1 \dots\ tn)} according to $\beta\iota\zeta$-reduction rules. 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 diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 3def7a48ad..59e0237628 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -438,6 +438,10 @@ let rec intro_then_gen loc name_flag move_flag force_flag dep_flag tac gl = gl | _ -> if not force_flag then raise (RefinerError IntroNeedsProduct); + (* Note: red_in_concl includes betaiotazeta and this was like *) + (* this since at least V6.3 (a pity *) + (* that intro do betaiotazeta only when reduction is needed; and *) + (* probably also a pity that intro does zeta *) try tclTHEN try_red_in_concl (intro_then_gen loc name_flag move_flag force_flag dep_flag tac) gl |