Skip to content
Snippets Groups Projects
Commit 93d78065 authored by Gregory Malecha's avatar Gregory Malecha
Browse files

Document the need for [Unset Universe Minimization ToSet].

parent b79d6540
No related branches found
No related tags found
1 merge request!368Define [tele_arg] as a fixpoint
Hide whitespace changes
Inline Side-by-side
Showing
with 3 additions and 0 deletions
theories/telescopes.v
+ 3
− 0
View file @ 93d78065
...@@ -2,6 +2,9 @@ From stdpp Require Import base tactics. ...@@ -2,6 +2,9 @@ From stdpp Require Import base tactics.
From stdpp Require Import options. From stdpp Require Import options.
Local Set Universe Polymorphism. Local Set Universe Polymorphism.
(* Without this flag, Coq minimizes some universes to [Set] when they
should not be, e.g. in [texist_exist]. *)
Local Unset Universe Minimization ToSet. Local Unset Universe Minimization ToSet.
(** Telescopes *) (** Telescopes *)
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment