aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-12-15 19:09:15 +0100
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-12-23 19:50:55 +0100
commit21750c40ee3f7ef3103121db68aef4339dceba40 (patch)
tree0d431861ae07801be81224e6123f151a24c84d41 /parsing
parentdea75d74c222c25f6aa6c38506ac7a51b339e9c6 (diff)
[api] Also deprecate constructors of Decl_kinds.
Unfortunately OCaml doesn't deprecate the constructors of a type when the type alias is deprecated. In this case it means that we don't get rid of the kernel dependency unless we deprecate the constructors too.
Diffstat (limited to 'parsing')
-rw-r--r--parsing/g_vernac.ml41
1 files changed, 1 insertions, 0 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index c18c6810f..29bcddaf4 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -15,6 +15,7 @@ open Constrexpr_ops
open Extend
open Vernacexpr
open Decl_kinds
+open Declarations
open Misctypes
open Tok (* necessary for camlp4 *)