diff options
| -rw-r--r-- | engine/uState.ml | 3 | ||||
| -rw-r--r-- | test-suite/success/polymorphism.v | 13 |
2 files changed, 16 insertions, 0 deletions
diff --git a/engine/uState.ml b/engine/uState.ml index 282acb3d6..ff91493ee 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 00cab744e..930c16517 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. |