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

(limited to 'vernac/comProgramFixpoint.mli')

diff --git a/vernac/comProgramFixpoint.mli b/vernac/comProgramFixpoint.mli
index 30bf3ae8f8..0193be8683 100644
--- a/vernac/comProgramFixpoint.mli
+++ b/vernac/comProgramFixpoint.mli
@@ -15,6 +15,7 @@ val do_fixpoint :
      pm:Declare.OblState.t
   -> scope:Locality.locality
   -> poly:bool
+  -> ?typing_flags:Declarations.typing_flags
   -> ?using:Vernacexpr.section_subset_expr
   -> fixpoint_expr list
   -> Declare.OblState.t
-- 
cgit v1.2.3