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/comInductive.mli | 1 +
 1 file changed, 1 insertion(+)

(limited to 'vernac/comInductive.mli')

diff --git a/vernac/comInductive.mli b/vernac/comInductive.mli
index 8bce884ba4..e049bacb26 100644
--- a/vernac/comInductive.mli
+++ b/vernac/comInductive.mli
@@ -26,6 +26,7 @@ val do_mutual_inductive
   -> (one_inductive_expr * decl_notation list) list
   -> cumulative:bool
   -> poly:bool
+  -> ?typing_flags:Declarations.typing_flags
   -> private_ind:bool
   -> uniform:uniform_inductive_flag
   -> Declarations.recursivity_kind
-- 
cgit v1.2.3