aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2018-05-31 10:59:24 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2018-05-31 10:59:24 +0200
commitac8a84e3b4dc530b000e17b72c7e26f7a957420f (patch)
treebaf58d74b6629034cecb577eade044f29313cc4d /vernac
parent22db6304ffd45d7ae6e4a0acf909afb1ec55d02c (diff)
parent0dc79e09b2b7c369b35191191aa257451a536540 (diff)
Merge PR #6969: [api] Remove functions deprecated in 8.8
Diffstat (limited to 'vernac')
-rw-r--r--vernac/vernacexpr.ml11
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"]