aboutsummaryrefslogtreecommitdiffhomepage
path: root/library
diff options
context:
space:
mode:
authorGravatar Matthieu Sozeau <mattam@mattam.org>2016-09-28 17:26:14 +0200
committerGravatar Matthieu Sozeau <mattam@mattam.org>2016-09-29 17:49:43 +0200
commitcf87e73ff4dd0b9c70436d66d326ae839868ba78 (patch)
tree1df8eeecc54c7cc1cf30af8a31800e3f694eaad9 /library
parent8e0f29cb69f06b64d74b18b09fb6a717034f1140 (diff)
Fix bug #5036 autorewrite, sections and universes
Universe context not properly declared. Improve API and code in declare.ml to allow declaration of universe contexts, used by declaration of universes and constraints (separately).
Diffstat (limited to 'library')
-rw-r--r--library/declare.ml26
-rw-r--r--library/declare.mli4
2 files changed, 24 insertions, 6 deletions
diff --git a/library/declare.ml b/library/declare.ml
index 3d063225f..7d32b93dc 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -434,6 +434,23 @@ let assumption_message id =
(** Global universe names, in a different summary *)
+type universe_context_decl = polymorphic * Univ.universe_context_set
+
+let cache_universe_context (p, ctx) =
+ Global.push_context_set p ctx;
+ if p then Lib.add_section_context ctx
+
+let input_universe_context : universe_context_decl -> Libobject.obj =
+ declare_object
+ { (default_object "Global universe context state") with
+ cache_function = (fun (na, pi) -> cache_universe_context pi);
+ load_function = (fun _ (_, pi) -> cache_universe_context pi);
+ discharge_function = (fun (_, (p, _ as x)) -> if p then None else Some x);
+ classify_function = (fun a -> Keep a) }
+
+let declare_universe_context poly ctx =
+ Lib.add_anonymous_leaf (input_universe_context (poly, ctx))
+
(* Discharged or not *)
type universe_decl = polymorphic * (Id.t * Univ.universe_level) list
@@ -446,9 +463,8 @@ let cache_universes (p, l) =
Univ.ContextSet.add_universe lev ctx))
(glob, Univ.ContextSet.empty) l
in
- Global.push_context_set p ctx;
- if p then Lib.add_section_context ctx;
- Universes.set_global_universe_names glob'
+ cache_universe_context (p, ctx);
+ Universes.set_global_universe_names glob'
let input_universes : universe_decl -> Libobject.obj =
declare_object
@@ -475,8 +491,8 @@ let do_universe poly l =
type constraint_decl = polymorphic * Univ.constraints
let cache_constraints (na, (p, c)) =
- Global.add_constraints c;
- if p then Lib.add_section_context (Univ.ContextSet.add_constraints c Univ.ContextSet.empty)
+ let ctx = Univ.ContextSet.add_constraints c Univ.ContextSet.empty in
+ cache_universe_context (p,ctx)
let discharge_constraints (_, (p, c as a)) =
if p then None else Some a
diff --git a/library/declare.mli b/library/declare.mli
index 7824506da..e614f5206 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -87,7 +87,9 @@ val exists_name : Id.t -> bool
-(** Global universe names and constraints *)
+(** Global universe contexts, names and constraints *)
+
+val declare_universe_context : polymorphic -> Univ.universe_context_set -> unit
val do_universe : polymorphic -> Id.t Loc.located list -> unit
val do_constraint : polymorphic -> (Id.t Loc.located * Univ.constraint_type * Id.t Loc.located) list -> unit