From 02e6d7f39e3dc2aa8859274bc69b2edf8cc91feb Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Sat, 16 Sep 2017 14:05:52 +0200
Subject: restrict_universe_context: do not prune named universes.

---
 engine/uState.ml                  |  3 +++
 test-suite/success/polymorphism.v | 13 +++++++++++++
 2 files changed, 16 insertions(+)

diff --git a/engine/uState.ml b/engine/uState.ml
index 282acb3d6e..ff91493ee5 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -315,6 +315,9 @@ let check_univ_decl uctx decl =
   ctx
 
 let restrict ctx vars =
+  let vars = Names.Id.Map.fold (fun na l vars -> Univ.LSet.add l vars)
+      (fst ctx.uctx_names) vars
+  in
   let uctx' = Univops.restrict_universe_context ctx.uctx_local vars in
   { ctx with uctx_local = uctx' }
 
diff --git a/test-suite/success/polymorphism.v b/test-suite/success/polymorphism.v
index 00cab744eb..930c165178 100644
--- a/test-suite/success/polymorphism.v
+++ b/test-suite/success/polymorphism.v
@@ -401,6 +401,19 @@ Module Anonymous.
 
 End Anonymous.
 
+Module Restrict.
+  (* Universes which don't appear in the term should be pruned, unless they have names *)
+  Set Universe Polymorphism.
+
+  Definition dummy_pruned@{} : nat := ltac:(let x := constr:(Type) in exact 0).
+
+  Definition named_not_pruned@{u} : nat := 0.
+  Check named_not_pruned@{_}.
+
+  Definition named_not_pruned_nonstrict : nat := ltac:(let x := constr:(Type@{u}) in exact 0).
+  Check named_not_pruned_nonstrict@{_}.
+End Restrict.
+
 Module F.
   Context {A B : Type}.
   Definition foo : Type := B.
-- 
cgit v1.2.3