diff options
Diffstat (limited to 'vernac/g_vernac.mlg')
| -rw-r--r-- | vernac/g_vernac.mlg | 40 |
1 files changed, 20 insertions, 20 deletions
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index 5b039e76f3..831aeff6a0 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -33,26 +33,26 @@ open Attributes (* Rem: do not join the different GEXTEND into one, it breaks native *) (* compilation on PowerPC and Sun architectures *) -let query_command = Entry.create "vernac:query_command" - -let search_query = Entry.create "vernac:search_query" -let search_queries = Entry.create "vernac:search_queries" - -let subprf = Entry.create "vernac:subprf" - -let quoted_attributes = Entry.create "vernac:quoted_attributes" -let class_rawexpr = Entry.create "vernac:class_rawexpr" -let thm_token = Entry.create "vernac:thm_token" -let def_token = Entry.create "vernac:def_token" -let assumption_token = Entry.create "vernac:assumption_token" -let def_body = Entry.create "vernac:def_body" -let decl_notations = Entry.create "vernac:decl_notations" -let record_field = Entry.create "vernac:record_field" -let of_type_with_opt_coercion = Entry.create "vernac:of_type_with_opt_coercion" -let section_subset_expr = Entry.create "vernac:section_subset_expr" -let scope_delimiter = Entry.create "vernac:scope_delimiter" -let syntax_modifiers = Entry.create "vernac:syntax_modifiers" -let only_parsing = Entry.create "vernac:only_parsing" +let query_command = Entry.create "query_command" + +let search_query = Entry.create "search_query" +let search_queries = Entry.create "search_queries" + +let subprf = Entry.create "subprf" + +let quoted_attributes = Entry.create "quoted_attributes" +let class_rawexpr = Entry.create "class_rawexpr" +let thm_token = Entry.create "thm_token" +let def_token = Entry.create "def_token" +let assumption_token = Entry.create "assumption_token" +let def_body = Entry.create "def_body" +let decl_notations = Entry.create "decl_notations" +let record_field = Entry.create "record_field" +let of_type_with_opt_coercion = Entry.create "of_type_with_opt_coercion" +let section_subset_expr = Entry.create "section_subset_expr" +let scope_delimiter = Entry.create "scope_delimiter" +let syntax_modifiers = Entry.create "syntax_modifiers" +let only_parsing = Entry.create "only_parsing" let make_bullet s = let open Proof_bullet in |
