1 files changed, 11 insertions, 0 deletions
diff --git a/test-suite/success/extraction_polyprop.v b/test-suite/success/extraction_polyprop.v
new file mode 100644
index 00000000..7215bd99
--- /dev/null
+++ b/test-suite/success/extraction_polyprop.v
@@ -0,0 +1,11 @@
+(* The current extraction cannot handle this situation,
+   and shouldn't try, otherwise it might produce some Ocaml
+   code that segfaults. See Table.error_singleton_become_prop
+   or S. Glondu's thesis for more details. *)
+
+Definition f {X} (p : (nat -> X) * True) : X * nat :=
+  (fst p 0, 0).
+
+Definition f_prop := f ((fun _ => I),I).
+
+Fail Extraction f_prop.