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.ml | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

(limited to 'vernac/comInductive.ml')

diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index 8cb077ca21..5c859e2f01 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -631,7 +631,7 @@ type uniform_inductive_flag =
   | UniformParameters
   | NonUniformParameters
 
-let do_mutual_inductive ~template udecl indl ~cumulative ~poly ~private_ind ~uniform finite =
+let do_mutual_inductive ~template udecl indl ~cumulative ~poly ?typing_flags ~private_ind ~uniform finite =
   let (params,indl),coes,ntns = extract_mutual_inductive_declaration_components indl in
   (* Interpret the types *)
   let indl = match params with
@@ -640,9 +640,11 @@ let do_mutual_inductive ~template udecl indl ~cumulative ~poly ~private_ind ~uni
       | UniformParameters -> (params, [], indl)
       | NonUniformParameters -> ([], params, indl)
   in
-  let mie,pl,impls = interp_mutual_inductive_gen (Global.env()) ~template udecl indl ntns ~cumulative ~poly ~private_ind finite in
+  let env = Global.env () in
+  let env = Option.cata (fun typing_flags -> Environ.set_typing_flags typing_flags env) env typing_flags in
+  let mie,pl,impls = interp_mutual_inductive_gen env ~template udecl indl ntns ~cumulative ~poly ~private_ind finite in
   (* Declare the mutual inductive block with its associated schemes *)
-  ignore (DeclareInd.declare_mutual_inductive_with_eliminations mie pl impls);
+  ignore (DeclareInd.declare_mutual_inductive_with_eliminations ?typing_flags mie pl impls);
   (* Declare the possible notations of inductive types *)
   List.iter (Metasyntax.add_notation_interpretation (Global.env ())) ntns;
   (* Declare the coercions *)
-- 
cgit v1.2.3


From 2ac3d11f6f1332250e918ef628eca3b788b3550a Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Fri, 16 Oct 2020 20:06:26 +0200
Subject: [environ] [typing_flags] Introduce helper function to remove
 duplicate code

---
 vernac/comInductive.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'vernac/comInductive.ml')

diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index 5c859e2f01..2be6097184 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -641,7 +641,7 @@ let do_mutual_inductive ~template udecl indl ~cumulative ~poly ?typing_flags ~pr
       | NonUniformParameters -> ([], params, indl)
   in
   let env = Global.env () in
-  let env = Option.cata (fun typing_flags -> Environ.set_typing_flags typing_flags env) env typing_flags in
+  let env = Environ.update_typing_flags ?typing_flags env in
   let mie,pl,impls = interp_mutual_inductive_gen env ~template udecl indl ntns ~cumulative ~poly ~private_ind finite in
   (* Declare the mutual inductive block with its associated schemes *)
   ignore (DeclareInd.declare_mutual_inductive_with_eliminations ?typing_flags mie pl impls);
-- 
cgit v1.2.3