From bdd943063ccd1309654b545819964c7c20752314 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 14 Dec 2018 14:00:14 +0100
Subject: Restrict body universes in delayed mode.

---
 test-suite/stm/delayed_restrict_univs_9093.v | 10 ++++++++++
 1 file changed, 10 insertions(+)
 create mode 100644 test-suite/stm/delayed_restrict_univs_9093.v

(limited to 'test-suite')

diff --git a/test-suite/stm/delayed_restrict_univs_9093.v b/test-suite/stm/delayed_restrict_univs_9093.v
new file mode 100644
index 0000000000..6ca36da4b0
--- /dev/null
+++ b/test-suite/stm/delayed_restrict_univs_9093.v
@@ -0,0 +1,10 @@
+(* -*- coq-prog-args: ("-async-proofs" "on"); -*- *)
+
+Unset Universe Polymorphism.
+
+Ltac exact0 := let x := constr:(Type) in exact 0.
+
+Lemma lemma_restrict_abstract@{} : (nat * nat)%type.
+Proof. split;[exact 0|abstract exact0]. Qed.
+(* Debug: 10237:proofworker:0:0 STM: sending back a fat state
+Error: Universe {polymorphism.1} is unbound. *)
-- 
cgit v1.2.3