diff options
| -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 21f15e7218..e86b3be64e 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 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) *) |