diff options
Diffstat (limited to 'intf')
| -rw-r--r-- | intf/constrexpr.ml | 7 | ||||
| -rw-r--r-- | intf/vernacexpr.ml | 16 |
2 files changed, 17 insertions, 6 deletions
diff --git a/intf/constrexpr.ml b/intf/constrexpr.ml index 474b80ec48..b0a769c5a8 100644 --- a/intf/constrexpr.ml +++ b/intf/constrexpr.ml @@ -17,6 +17,11 @@ open Decl_kinds (** [constr_expr] is the abstract syntax tree produced by the parser *) +type universe_decl_expr = (lident list, glob_constraint list) gen_universe_decl + +type ident_decl = lident * universe_decl_expr option +type name_decl = lname * universe_decl_expr option + type notation = string type explicitation = @@ -139,7 +144,7 @@ type constr_pattern_expr = constr_expr type with_declaration_ast = | CWith_Module of Id.t list Loc.located * qualid Loc.located - | CWith_Definition of Id.t list Loc.located * constr_expr + | CWith_Definition of Id.t list Loc.located * universe_decl_expr option * constr_expr type module_ast_r = | CMident of qualid diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml index 7e9bc8caa9..0a6e5b3b31 100644 --- a/intf/vernacexpr.ml +++ b/intf/vernacexpr.ml @@ -160,11 +160,6 @@ type option_ref_value = (** Identifier and optional list of bound universes and constraints. *) -type universe_decl_expr = (lident list, glob_constraint list) gen_universe_decl - -type ident_decl = lident * universe_decl_expr option -type name_decl = lname * universe_decl_expr option - type sort_expr = Sorts.family type definition_expr = @@ -536,3 +531,14 @@ type vernac_when = | VtNow | VtLater type vernac_classification = vernac_type * vernac_when + + +(** Deprecated stuff *) +type universe_decl_expr = Constrexpr.universe_decl_expr +[@@ocaml.deprecated "alias of Constrexpr.universe_decl_expr"] + +type ident_decl = Constrexpr.ident_decl +[@@ocaml.deprecated "alias of Constrexpr.ident_decl"] + +type name_decl = Constrexpr.name_decl +[@@ocaml.deprecated "alias of Constrexpr.name_decl"] |