From 0ca664107a1e60dfa47aa7536e30a348456efe44 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 9 Nov 2020 21:36:51 +0100
Subject: Fix #13330: Kernel messes with polymorphic side-effects.

Polymorphic side-effects generated in monomorphic mode would be counted towards
trusted subcomponents. This would allow to make ill-typed terms pass as
legitimate by mimicking the shape of the inlining of monomorphic side-effects in
such a proof.
---
 test-suite/bugs/closed/bug_13330.v | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)
 create mode 100644 test-suite/bugs/closed/bug_13330.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/bug_13330.v b/test-suite/bugs/closed/bug_13330.v
new file mode 100644
index 0000000000..d13de2e58d
--- /dev/null
+++ b/test-suite/bugs/closed/bug_13330.v
@@ -0,0 +1,17 @@
+Polymorphic Inductive path {A : Type} (x : A) : A -> Type :=
+  refl : path x x.
+
+Goal False.
+Proof.
+simple refine (let H : False := _ in _).
++ exact_no_check I.
++ assert (path true false -> path false true).
+  (** Create a dummy polymorphic side-effect *)
+  {
+    intro IHn.
+    rewrite IHn.
+    reflexivity.
+  }
+  exact H.
+Fail Qed.
+Abort.
-- 
cgit v1.2.3