diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-03-23 16:49:56 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-03-23 16:49:56 +0000 |
| commit | 263ec91e6664a9f1f8823c791690cb5ddf43c547 (patch) | |
| tree | d3a6d5df93ccb9701cb00f1e563bcf866d40dfdf /checker/mod_checking.ml | |
| parent | 4aa0debbae28fa5768d2ce3f9ffe82d2a015ce39 (diff) | |
Fix the test-suite by removing any Reset in the scripts
Reset and the other backtracking commands (Back, BackTo, Backtrack)
are now allowed only during interactive session, not in compiled
or loaded scripts.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15087 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'checker/mod_checking.ml')
0 files changed, 0 insertions, 0 deletions