diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-03-21 19:12:58 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-03-21 19:12:58 +0000 |
| commit | f687552465f86bfd66ada997a26486b2a20d5363 (patch) | |
| tree | 026113c71989f20ec0073a72ffad606868d2de94 /doc/refman | |
| 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 'doc/refman')
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index d59e62640..a2d02a4ca 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. |