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.

1 files changed, 20 insertions, 0 deletions

diff --git a/engine/evd.ml b/engine/evd.ml
index cfc9aa6351..06b257a9e5 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -750,6 +750,26 @@ let universe_context_set d = UState.context_set d.universes
 
 let universe_context ?names evd = UState.universe_context ?names evd.universes
 
+open Misctypes
+type universe_decl =
+  (Names.Id.t Loc.located list, Univ.Constraint.t) Misctypes.gen_universe_decl
+
+let check_implication evd cstrs ctx =
+  let uctx = evar_universe_context evd in
+  let gr = UState.initial_graph uctx in
+  let grext = UGraph.merge_constraints cstrs gr in
+  let cstrs' = Univ.UContext.constraints ctx in
+  if UGraph.check_constraints cstrs' grext then ()
+  else CErrors.user_err ~hdr:"check_univ_decl"
+                  (str "Universe constraints are not implied by the ones declared.")
+
+let check_univ_decl evd decl =
+  let pl = if decl.univdecl_extensible_instance then None else Some decl.univdecl_instance in
+  let pl, ctx = universe_context ?names:pl evd in
+  if not decl.univdecl_extensible_constraints then
+    check_implication evd decl.univdecl_constraints ctx;
+  pl, ctx
+
 let restrict_universe_context evd vars =
   { evd with universes = UState.restrict evd.universes vars }