diff options
Diffstat (limited to 'vernac/vernacexpr.ml')
| -rw-r--r-- | vernac/vernacexpr.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml index 2287630c7..e97cac818 100644 --- a/vernac/vernacexpr.ml +++ b/vernac/vernacexpr.ml @@ -459,7 +459,7 @@ type nonrec vernac_expr = (* For extension *) | VernacExtend of extend_name * Genarg.raw_generic_argument list -type vernac_flags = (Names.Id.t * vernac_flag_value) list +type vernac_flags = (string * vernac_flag_value) list and vernac_flag_value = | VernacFlagEmpty | VernacFlagLeaf of string |