diff options
| author | lmamane | 2007-02-22 12:19:52 +0000 |
|---|---|---|
| committer | lmamane | 2007-02-22 12:19:52 +0000 |
| commit | 8ba8385acc7e71fccdb72bfa0908e4f64400c633 (patch) | |
| tree | f078c69c852d30ad97e5005dfe7b41c62f1d3bc2 /kernel/cbytecodes.ml | |
| parent | 09ceaf1bac341c66c5d733f0358fc9b4b3dbad93 (diff) | |
Documentation of tactical "t1 || t2": t2 is executed if t1 fails to
progress, not only if it fails (i.e. gives an error).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9670 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/cbytecodes.ml')
0 files changed, 0 insertions, 0 deletions