diff options
| -rw-r--r-- | test-suite/success/unification.v | 8 |
1 files changed, 0 insertions, 8 deletions
diff --git a/test-suite/success/unification.v b/test-suite/success/unification.v index 3d935cd1da..91ee18ea46 100644 --- a/test-suite/success/unification.v +++ b/test-suite/success/unification.v @@ -126,11 +126,3 @@ intros. exists (fun n => match n with O => a | S n' => f' n' end). constructor. Qed. - -(* Why this not work, even, without the "fix" to #1851 *) - -Goal forall X (a:X 0) (f':forall n:nat, X n), (exists f : forall n:nat, X n, True). -intros. -exists (fun n => match n with O => a | S n' => f' n' end). -constructor. -Qed. |