Merge PR #13331: Fix #13330: Kernel messes with polymorphic side-effects.

Reviewed-by: Zimmi48
Reviewed-by: SkySkimmer
Ack-by: gares
Ack-by: jfehrle
Ack-by: jashug
Ack-by: ejgallego

1 files changed, 17 insertions, 0 deletions

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.