aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2017-11-21 13:58:08 +0100
committerGravatar Maxime Dénès <mail@maximedenes.fr>2017-11-21 13:58:08 +0100
commitb75beb248873db7d9ab8e4a078022b2ed0edcd36 (patch)
tree4d2bc9d39c1f6d7c4d00223143f18ae5bad500e5 /vernac
parent0e01de69c22a3793855b4c97c50e4514191b19bc (diff)
parent094b577f61f105f0a92f3f84d7e739884dd993a7 (diff)
Merge PR #6185: [parser] Remove unnecessary statically initialized hook.
Diffstat (limited to 'vernac')
-rw-r--r--vernac/command.ml1
1 files changed, 0 insertions, 1 deletions
diff --git a/vernac/command.ml b/vernac/command.ml
index b027863e8..fd0027c40 100644
--- a/vernac/command.ml
+++ b/vernac/command.ml
@@ -22,7 +22,6 @@ open Globnames
open Nameops
open Constrexpr
open Constrexpr_ops
-open Topconstr
open Constrintern
open Nametab
open Impargs