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. --- interp/dumpglob.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'interp/dumpglob.mli') 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 -- cgit v1.2.3