diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2017-07-27 14:54:41 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2017-09-19 10:28:03 +0200 |
| commit | f72a67569ec8cb9160d161699302b67919da5686 (patch) | |
| tree | a86642e048c3ac571829e6b1eb6f3d53a34d3db0 /engine/universes.ml | |
| parent | fc587e75d2d5d6e67365a9bc3a13ba5c86aba87b (diff) | |
Allow declaring universe constraints at definition level.
Introduce a "+" modifier for universe and constraint declarations to
indicate that these can be extended in the final definition/proof. By
default [Definition f] is equivalent to [Definition f@{+|+}], i.e
universes can be introduced and constraints as well. For [f@{}] or
[f@{i j}], the constraints can be extended, no universe introduced, to
maintain compatibility with existing developments. Use [f@{i j | }] to
indicate that no constraint (nor universe) can be introduced. These
kind of definitions could benefit from asynchronous processing.
Declarations of universe binders and constraints also works for
monomorphic definitions.
Diffstat (limited to 'engine/universes.ml')
| -rw-r--r-- | engine/universes.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/engine/universes.ml b/engine/universes.ml index 719af43ed..91398d162 100644 --- a/engine/universes.ml +++ b/engine/universes.ml @@ -14,7 +14,7 @@ open Environ open Univ open Globnames -let pr_with_global_universes l = +let pr_with_global_universes l = try Nameops.pr_id (LMap.find l (snd (Global.global_universe_names ()))) with Not_found -> Level.pr l @@ -31,7 +31,7 @@ let universe_binders_of_global ref = let register_universe_binders ref l = universe_binders_table := Refmap.add ref l !universe_binders_table - + (* To disallow minimization to Set *) let set_minimization = ref true |