diff options
| author | Arnaud Spiwack | 2013-12-06 11:04:35 +0100 |
|---|---|---|
| committer | Arnaud Spiwack | 2013-12-06 14:14:56 +0100 |
| commit | a6a87649c3e0ea205e0ad9e9536bb881ddc2e73b (patch) | |
| tree | 1012fe01b3dabe56b50835c6b0fde12526e81649 /test-suite/success | |
| parent | 079543c80e6bee4a4e5707bcac17a965b786077f (diff) | |
Fix the refine related test-suite files to account for the new refine.
Diffstat (limited to 'test-suite/success')
| -rw-r--r-- | test-suite/success/TestRefine.v | 2 | ||||
| -rw-r--r-- | test-suite/success/refine.v | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/test-suite/success/TestRefine.v b/test-suite/success/TestRefine.v index 2ad643f34c..213b528301 100644 --- a/test-suite/success/TestRefine.v +++ b/test-suite/success/TestRefine.v @@ -176,7 +176,7 @@ Restart. end). exists 1. trivial. -elim (f0 p). +elim (f p). refine (fun (x : nat) (h : x = S p) => exist (fun x : nat => x = S (S p)) (S x) _). rewrite h. auto. diff --git a/test-suite/success/refine.v b/test-suite/success/refine.v index 352abb2af5..1e667884b8 100644 --- a/test-suite/success/refine.v +++ b/test-suite/success/refine.v @@ -62,7 +62,7 @@ Abort. Goal (forall n : nat, n = 0 -> Prop) -> Prop. intro P. refine (P _ _). -reflexivity. +2:reflexivity. Abort. (* Submitted by Jacek Chrzaszcz (bug #1102) *) |