diff options
Diffstat (limited to 'test-suite/failure/fixpoint4.v')
| -rw-r--r-- | test-suite/failure/fixpoint4.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/failure/fixpoint4.v b/test-suite/failure/fixpoint4.v index fd956373..bf6133f1 100644 --- a/test-suite/failure/fixpoint4.v +++ b/test-suite/failure/fixpoint4.v @@ -8,7 +8,7 @@ Inductive IMP : Prop := Definition i0 := (LIMP (fun _ => CIMP (fun _ x => x))). -Definition Paradox : False := +Fail Definition Paradox : False := (fix F y o {struct o} : False := match y with | tt => fun f => |