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.

---
 proofs/proof_global.ml                       | 14 +++++++++++---
 test-suite/stm/delayed_restrict_univs_9093.v | 10 ++++++++++
 2 files changed, 21 insertions(+), 3 deletions(-)
 create mode 100644 test-suite/stm/delayed_restrict_univs_9093.v

diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 8077da8807..bea5580074 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -339,6 +339,7 @@ let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now
     Proof.in_proof proof (fun m -> Evd.existential_opt_value0 m k) in
   let nf = UnivSubst.nf_evars_and_universes_opt_subst subst_evar
     (UState.subst universes) in
+
   let make_body =
     if poly || now then
       let make_body t (c, eff) =
@@ -386,14 +387,21 @@ let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now
       fun t p ->
         (* Already checked the univ_decl for the type universes when starting the proof. *)
         let univctx = Entries.Monomorphic_const_entry (UState.context_set universes) in
-        Future.from_val (univctx, nf t),
+        let t = nf t in
+        Future.from_val (univctx, t),
         Future.chain p (fun (pt,eff) ->
           (* Deferred proof, we already checked the universe declaration with
              the initial universes, ensure that the final universes respect
              the declaration as well. If the declaration is non-extensible,
              this will prevent the body from adding universes and constraints. *)
-          let bodyunivs = constrain_variables (Future.force univs) in
-          let univs = UState.check_mono_univ_decl bodyunivs universe_decl in
+          let univs = Future.force univs in
+          let univs = constrain_variables univs in
+          let used_univs = Univ.LSet.union
+              (Vars.universes_of_constr t)
+              (Vars.universes_of_constr pt)
+          in
+          let univs = UState.restrict univs used_univs in
+          let univs = UState.check_mono_univ_decl univs universe_decl in
           (pt,univs),eff)
   in
   let entry_fn p (_, t) =
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