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/bugs | |
| parent | 079543c80e6bee4a4e5707bcac17a965b786077f (diff) | |
Fix the refine related test-suite files to account for the new refine.
Diffstat (limited to 'test-suite/bugs')
| -rw-r--r-- | test-suite/bugs/closed/931.v | 2 |
1 files changed, 1 insertions, 1 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. |