summaryrefslogtreecommitdiff
path: root/test-suite/failure/fixpoint3.v
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/failure/fixpoint3.v')
-rw-r--r--test-suite/failure/fixpoint3.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/failure/fixpoint3.v b/test-suite/failure/fixpoint3.v
index 42f06916..7d1d3ee6 100644
--- a/test-suite/failure/fixpoint3.v
+++ b/test-suite/failure/fixpoint3.v
@@ -6,7 +6,7 @@ Inductive I : Prop :=
Definition i0 := C (fun _ x => x).
-Definition Paradox : False :=
+Fail Definition Paradox : False :=
(fix ni i : False :=
match i with
| C f => ni (f _ i)