9 files changed, 74 insertions, 0 deletions
diff --git a/test-suite/ltac2/example2.v b/test-suite/ltac2/example2.v
index c953d25061..ac92ca34ef 100644
--- a/test-suite/ltac2/example2.v
+++ b/test-suite/ltac2/example2.v
@@ -261,6 +261,25 @@ assert (H : 0 + 0 = 0) by reflexivity.
 intros x; exact x.
 Qed.
 
+Goal True.
+Proof.
+enough (H := 0 + 0).
+constructor.
+Qed.
+
+Goal True.
+Proof.
+enough (exists n, n = 0) as [n Hn].
++ exact I.
++ exists 0; reflexivity.
+Qed.
+
+Goal True -> True.
+Proof.
+enough (H : 0 + 0 = 0) by (intros x; exact x).
+reflexivity.
+Qed.
+
 Goal 1 + 1 = 2.
 Proof.
 change (?a + 1 = 2) with (2 = $a + 1).
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}.
diff --git a/test-suite/output/RealSyntax.out b/test-suite/output/RealSyntax.out
index 2d877bd813..2b14ca7069 100644
--- a/test-suite/output/RealSyntax.out
+++ b/test-suite/output/RealSyntax.out
@@ -2,6 +2,8 @@
      : R
 (-31)%R
      : R
+15e-1%R
+     : R
 eq_refl : 102e-2 = 102e-2
      : 102e-2 = 102e-2
 eq_refl : 102e-1 = 102e-1
diff --git a/test-suite/output/RealSyntax.v b/test-suite/output/RealSyntax.v
index cb3bce70d4..7be8b18ac8 100644
--- a/test-suite/output/RealSyntax.v
+++ b/test-suite/output/RealSyntax.v
@@ -2,6 +2,8 @@ Require Import Reals.Rdefinitions.
 Check 32%R.
 Check (-31)%R.
 
+Check 1.5_%R.
+
 Open Scope R_scope.
 
 Check (eq_refl : 1.02 = IZR 102 / IZR (Z.pow_pos 10 2)).