diff options
| author | Gaëtan Gilbert | 2018-10-11 19:08:33 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-11-02 13:26:16 +0100 |
| commit | c44080b74f4ea1e4b7ae88dfe5a440364bed3fca (patch) | |
| tree | a14664e5bb5165415d2b1928fc0f2896e6ec36c1 /vernac/attributes.mli | |
| parent | 1808904b3088595f89c24aa25bffcc54b2b48fda (diff) | |
Universe Polymorphism is a normal attribute modulo the stm (no Flags)
Diffstat (limited to 'vernac/attributes.mli')
| -rw-r--r-- | vernac/attributes.mli | 10 |
1 files changed, 7 insertions, 3 deletions
diff --git a/vernac/attributes.mli b/vernac/attributes.mli index 27b873bfe0..c81082d5ad 100644 --- a/vernac/attributes.mli +++ b/vernac/attributes.mli @@ -47,9 +47,6 @@ val universe_poly_template : (bool * bool option) attribute val locality : bool option attribute val deprecation : deprecation option attribute -val polymorphic_nowarn : bool option attribute -(** For internal use, avoid warning if not qualified as eg [universes(polymorphic)]. *) - val program_opt : bool option attribute (** For internal use when messing with the global option. *) @@ -127,3 +124,10 @@ val make_attribute : (vernac_flags -> vernac_flags * 'a) -> 'a attribute (** Compatibility values for parsing [Polymorphic]. *) val vernac_polymorphic_flag : vernac_flag val vernac_monomorphic_flag : vernac_flag + +(** For the stm, do not use! *) + +val polymorphic_nowarn : bool attribute +(** For internal use, avoid warning if not qualified as eg [universes(polymorphic)]. *) +val universe_polymorphism_option_name : string list +val is_universe_polymorphism : unit -> bool |