diff options
| author |  Arnaud Spiwack <arnaud@spiwack.net> | 2013-12-06 11:04:35 +0100 |
|---|---|---|
| committer | Arnaud Spiwack <arnaud@spiwack.net> | 2013-12-06 14:14:56 +0100 |
| commit | a6a87649c3e0ea205e0ad9e9536bb881ddc2e73b (patch) | |
| tree | 1012fe01b3dabe56b50835c6b0fde12526e81649 /test-suite | |
| parent | 079543c80e6bee4a4e5707bcac17a965b786077f (diff) | |
Fix the refine related test-suite files to account for the new refine.
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/bugs/closed/931.v | 2 | ||||
| -rw-r--r-- | test-suite/success/TestRefine.v | 2 | ||||
| -rw-r--r-- | test-suite/success/refine.v | 2 |
3 files changed, 3 insertions, 3 deletions
diff --git a/test-suite/bugs/closed/931.v b/test-suite/bugs/closed/931.v index 21f15e721..e86b3be64 100644 --- a/test-suite/bugs/closed/931.v +++ b/test-suite/bugs/closed/931.v @@ -2,6 +2,6 @@ Parameter P : forall n : nat, n=n -> Prop. Goal Prop. refine (P _ _). - instantiate (1:=0). + 2:instantiate (1:=0). trivial. Qed. diff --git a/test-suite/success/TestRefine.v b/test-suite/success/TestRefine.v index 2ad643f34..213b52830 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 352abb2af..1e667884b 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) *) |