From 14150241cfd016c7f64974cc5c58bb116689f3c1 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 2 Jul 2020 18:17:24 +0200
Subject: [vernac] Allow to control typing flags with attributes.

The syntax is the one of boolean attributes, that is to say
`#[typing($flag={yes,no}]` where `$flag` is one of `guarded`,
`universes`, `positive`.

We had to instrument the pretyper in a few places, it is interesting
that it is doing so many checks.
---
 vernac/comDefinition.mli | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'vernac/comDefinition.mli')

diff --git a/vernac/comDefinition.mli b/vernac/comDefinition.mli
index 5e1b705ae4..9962e44098 100644
--- a/vernac/comDefinition.mli
+++ b/vernac/comDefinition.mli
@@ -30,6 +30,7 @@ val do_definition
   -> name:Id.t
   -> scope:Locality.locality
   -> poly:bool
+  -> ?typing_flags:Declarations.typing_flags
   -> kind:Decls.definition_object_kind
   -> ?using:Vernacexpr.section_subset_expr
   -> universe_decl_expr option
@@ -45,6 +46,7 @@ val do_definition_program
   -> name:Id.t
   -> scope:Locality.locality
   -> poly:bool
+  -> ?typing_flags:Declarations.typing_flags
   -> kind:Decls.logical_kind
   -> ?using:Vernacexpr.section_subset_expr
   -> universe_decl_expr option
-- 
cgit v1.2.3