Imported Upstream snapshot 8.3~beta0+13298

1 files changed, 13 insertions, 0 deletions

diff --git a/test-suite/failure/fixpoint3.v b/test-suite/failure/fixpoint3.v
new file mode 100644
index 00000000..42f06916
--- /dev/null
+++ b/test-suite/failure/fixpoint3.v
@@ -0,0 +1,13 @@
+(* Check that arguments of impredicative types are not considered
+   subterms for the guard condition (an example by Thierry Coquand) *)
+
+Inductive I : Prop :=
+| C: (forall P:Prop, P->P) -> I.
+
+Definition i0 := C (fun _ x => x).
+
+Definition Paradox : False :=
+ (fix ni i : False :=
+  match i with
+  | C f => ni (f _ i)
+  end) i0.