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 /test-suite/success/hyps_inclusion.v | |
| 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 'test-suite/success/hyps_inclusion.v')
| -rw-r--r-- | test-suite/success/hyps_inclusion.v | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/test-suite/success/hyps_inclusion.v b/test-suite/success/hyps_inclusion.v index af81e53d6..ebd90a40e 100644 --- a/test-suite/success/hyps_inclusion.v +++ b/test-suite/success/hyps_inclusion.v @@ -19,14 +19,16 @@ red in H. (* next tactic was failing wrt bug #1325 because type-checking the goal detected a syntactically different type for the section variable H *) case 0. -Reset A. +Abort. +End A. (* Variant with polymorphic inductive types for bug #1325 *) -Section A. +Section B. Variable H:not True. Inductive I (n:nat) : Type := C : H=H -> I n. Goal I 0. red in H. case 0. -Reset A. +Abort. +End B. |