From f72a67569ec8cb9160d161699302b67919da5686 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 27 Jul 2017 14:54:41 +0200
Subject: 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.
---
 API/API.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'API/API.ml')

diff --git a/API/API.ml b/API/API.ml
index 68da858ba0..46ad36d36d 100644
--- a/API/API.ml
+++ b/API/API.ml
@@ -162,6 +162,7 @@ module Indrec = Indrec
 (* module Cases *)
 module Pretyping = Pretyping
 module Unification = Unification
+module Univdecls = Univdecls
 (******************************************************************************)
 (* interp                                                                     *)
 (******************************************************************************)
-- 
cgit v1.2.3