From 332bb8c5199eb264d09d2810546170e0654f4527 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 10 Nov 2020 13:35:35 +0100
Subject: Add the test as a misc script.

I left the other test as a v file since it might become relevant when the
corresponding Qed bug is fixed.
---
 test-suite/misc/13330.sh          | 10 ++++++++++
 test-suite/misc/13330/bug_13330.v | 16 ++++++++++++++++
 2 files changed, 26 insertions(+)
 create mode 100755 test-suite/misc/13330.sh
 create mode 100644 test-suite/misc/13330/bug_13330.v

diff --git a/test-suite/misc/13330.sh b/test-suite/misc/13330.sh
new file mode 100755
index 0000000000..7340559432
--- /dev/null
+++ b/test-suite/misc/13330.sh
@@ -0,0 +1,10 @@
+#!/usr/bin/env bash
+
+$coqc misc/13330/bug_13330.v
+R=$?
+
+if [ $R == 0 ]; then
+  exit 1
+else
+  exit 0
+fi
diff --git a/test-suite/misc/13330/bug_13330.v b/test-suite/misc/13330/bug_13330.v
new file mode 100644
index 0000000000..acf6e80c48
--- /dev/null
+++ b/test-suite/misc/13330/bug_13330.v
@@ -0,0 +1,16 @@
+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.
+Qed.
-- 
cgit v1.2.3