aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp
diff options
context:
space:
mode:
authorGravatar Matthieu Sozeau <mattam@mattam.org>2017-07-27 14:54:41 +0200
committerGravatar Matthieu Sozeau <mattam@mattam.org>2017-09-19 10:28:03 +0200
commitf72a67569ec8cb9160d161699302b67919da5686 (patch)
treea86642e048c3ac571829e6b1eb6f3d53a34d3db0 /interp
parentfc587e75d2d5d6e67365a9bc3a13ba5c86aba87b (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 'interp')
-rw-r--r--interp/dumpglob.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/dumpglob.mli b/interp/dumpglob.mli
index 054e43e7c..afcd7a2ed 100644
--- a/interp/dumpglob.mli
+++ b/interp/dumpglob.mli
@@ -37,7 +37,7 @@ val dump_notation :
(Constrexpr.notation * Notation.notation_location) Loc.located ->
Notation_term.scope_name option -> bool -> unit
val dump_constraint :
- Constrexpr.typeclass_constraint -> bool -> string -> unit
+ Vernacexpr.typeclass_constraint -> bool -> string -> unit
val dump_string : string -> unit