aboutsummaryrefslogtreecommitdiff
path: root/vernac/attributes.mli
diff options
context:
space:
mode:
Diffstat (limited to 'vernac/attributes.mli')
-rw-r--r--vernac/attributes.mli3
1 files changed, 2 insertions, 1 deletions
diff --git a/vernac/attributes.mli b/vernac/attributes.mli
index 34ff15ca7d..0074db66d3 100644
--- a/vernac/attributes.mli
+++ b/vernac/attributes.mli
@@ -48,7 +48,8 @@ val program : bool attribute
val template : bool option attribute
val locality : bool option attribute
val deprecation : Deprecation.t option attribute
-val canonical : bool attribute
+val canonical_field : bool attribute
+val canonical_instance : bool attribute
val program_mode_option_name : string list
(** For internal use when messing with the global option. *)