summaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed/shouldsucceed/1776.v
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/bugs/closed/shouldsucceed/1776.v')
-rw-r--r--test-suite/bugs/closed/shouldsucceed/1776.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/bugs/closed/shouldsucceed/1776.v b/test-suite/bugs/closed/shouldsucceed/1776.v
index abf85455..58491f9d 100644
--- a/test-suite/bugs/closed/shouldsucceed/1776.v
+++ b/test-suite/bugs/closed/shouldsucceed/1776.v
@@ -10,7 +10,7 @@ Definition nexists (P:nat -> nat -> Prop) : nat -> Prop :=
Goal forall a A m,
True ->
- (pl A (nexists (fun x => (nexists
+ (pl A (nexists (fun x => (nexists
(fun y => pl (pair a (S x)) (pair a (S y))))))) m.
Proof.
intros.