From fb08d2d78c80f384e8ac2b7a9563b6c6720608f4 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Wed, 1 Nov 2017 15:26:40 +0100
Subject: [API] Some reordering following latest separation commits.

We can now place most of intf modules just after `Libnames/Globnames`
which is quite low on the hierarchy.

A exception is `Vernacexpr` which still depends on `Extend` and
`GOptions`.
---
 API/API.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'API/API.ml')

diff --git a/API/API.ml b/API/API.ml
index 6e61063e4b..9a67e3111f 100644
--- a/API/API.ml
+++ b/API/API.ml
@@ -80,6 +80,7 @@ module Locus = Locus
 module Glob_term = Glob_term
 module Extend = Extend
 module Misctypes = Misctypes
+module Pattern = Pattern
 module Decl_kinds = Decl_kinds
 module Vernacexpr = Vernacexpr
 module Notation_term = Notation_term
@@ -118,8 +119,6 @@ module Universes = Universes
 module UState = UState
 module Evd = Evd
 module EConstr = EConstr
-module Tactypes = Tactypes
-module Pattern = Pattern
 module Namegen = Namegen
 module Termops = Termops
 module Proofview_monad = Proofview_monad
@@ -167,6 +166,7 @@ module Univdecls = Univdecls
 (******************************************************************************)
 (* interp                                                                     *)
 (******************************************************************************)
+module Tactypes = Tactypes
 module Stdarg = Stdarg
 module Genintern = Genintern
 module Constrexpr_ops = Constrexpr_ops
-- 
cgit v1.2.3