From 5b8b02cd060097c3c980b0498257c30eda1ad207 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 5 Dec 2017 20:22:14 +0100
Subject: Fix #6323: stronger restrict universe context vs abstract.

In the test we do [let X : Type@{i} := Set in ...] with Set
abstracted. The constraint [Set < i] was lost in the abstract.

Universes of a monomorphic reference [c] are considered to appear in
the term [c].
---
 proofs/pfedit.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'proofs/pfedit.ml')

diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 31a73db04f..6b503a0112 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -140,6 +140,7 @@ let build_constant_by_tactic id ctx sign ?(goal_kind = Global, false, Proof Theo
     let status = by tac in
     let _,(const,univs,_) = cook_proof () in
     Proof_global.discard_current ();
+    let univs = UState.demote_seff_univs const univs in
     const, status, univs
   with reraise ->
     let reraise = CErrors.push reraise in
-- 
cgit v1.2.3