Adding a test to the test-suite.

We take inspiration and code from the Evil plugin.

6 files changed, 51 insertions, 0 deletions

diff --git a/test-suite/misc/side-eff-leak-univs.sh b/test-suite/misc/side-eff-leak-univs.sh
new file mode 100755
index 0000000000..a0f7a8587c
--- /dev/null
+++ b/test-suite/misc/side-eff-leak-univs.sh
@@ -0,0 +1,19 @@
+#!/usr/bin/env bash
+
+set -e
+
+export COQBIN=$BIN
+export PATH=$COQBIN:$PATH
+
+cd misc/side-eff-leak-univs/
+
+coq_makefile -f _CoqProject -o Makefile
+
+make clean
+
+make src/evil_plugin.cma
+
+if make; then
+    >&2 echo 'Should have failed!'
+    exit 1
+fi
diff --git a/test-suite/misc/side-eff-leak-univs/.gitignore b/test-suite/misc/side-eff-leak-univs/.gitignore
new file mode 100644
index 0000000000..2a6a6bc68d
--- /dev/null
+++ b/test-suite/misc/side-eff-leak-univs/.gitignore
@@ -0,0 +1,2 @@
+/Makefile*
+/src/evil.ml
diff --git a/test-suite/misc/side-eff-leak-univs/_CoqProject b/test-suite/misc/side-eff-leak-univs/_CoqProject
new file mode 100644
index 0000000000..2099d862b2
--- /dev/null
+++ b/test-suite/misc/side-eff-leak-univs/_CoqProject
@@ -0,0 +1,6 @@
+-Q theories Evil
+-I src
+
+src/evil.mlg
+src/evil_plugin.mlpack
+theories/evil.v
diff --git a/test-suite/misc/side-eff-leak-univs/src/evil.mlg b/test-suite/misc/side-eff-leak-univs/src/evil.mlg
new file mode 100644
index 0000000000..d89ab887a8
--- /dev/null
+++ b/test-suite/misc/side-eff-leak-univs/src/evil.mlg
@@ -0,0 +1,13 @@
+DECLARE PLUGIN "evil_plugin"
+
+{
+open Ltac_plugin
+open Stdarg
+}
+
+TACTIC EXTEND magic
+| [ "magic" ident(i) ident(j) ] -> {
+  let open Glob_term in
+  DeclareUniv.do_constraint ~poly:false [ GType (Libnames.qualid_of_ident i), Univ.Lt, GType (Libnames.qualid_of_ident j)]; Proofview.tclUNIT()
+}
+END
diff --git a/test-suite/misc/side-eff-leak-univs/src/evil_plugin.mlpack b/test-suite/misc/side-eff-leak-univs/src/evil_plugin.mlpack
new file mode 100644
index 0000000000..6382aa69e1
--- /dev/null
+++ b/test-suite/misc/side-eff-leak-univs/src/evil_plugin.mlpack
@@ -0,0 +1 @@
+Evil
diff --git a/test-suite/misc/side-eff-leak-univs/theories/evil.v b/test-suite/misc/side-eff-leak-univs/theories/evil.v
new file mode 100644
index 0000000000..d138091fa9
--- /dev/null
+++ b/test-suite/misc/side-eff-leak-univs/theories/evil.v
@@ -0,0 +1,10 @@
+Declare ML Module "evil_plugin".
+
+Universes i j.
+
+Lemma foo@{} : Type@{j}.
+Proof.
+  magic i j; transparent_abstract exact_no_check Type@{i}.
+Defined.
+
+Definition bar : Type@{i} := Type@{j}.