diff options
Diffstat (limited to 'vernac/vernacexpr.ml')
| -rw-r--r-- | vernac/vernacexpr.ml | 11 |
1 files changed, 0 insertions, 11 deletions
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml index 40fab1f9c..4ff9d105b 100644 --- a/vernac/vernacexpr.ml +++ b/vernac/vernacexpr.ml @@ -520,14 +520,3 @@ 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"] |