From 615290d0f9d5cad7c508d45cf4ab89aecff033b2 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Fri, 1 Jun 2018 02:37:15 +0200
Subject: [api] Remove Misctypes.

We move the last 3 types to more adequate places.
---
 vernac/g_vernac.ml4      | 1 -
 vernac/vernacentries.ml  | 3 +--
 vernac/vernacentries.mli | 4 +---
 vernac/vernacexpr.ml     | 1 -
 4 files changed, 2 insertions(+), 7 deletions(-)

(limited to 'vernac')

diff --git a/vernac/g_vernac.ml4 b/vernac/g_vernac.ml4
index 59449d07af..3a59242de5 100644
--- a/vernac/g_vernac.ml4
+++ b/vernac/g_vernac.ml4
@@ -20,7 +20,6 @@ open Extend
 open Decl_kinds
 open Declaremods
 open Declarations
-open Misctypes
 open Namegen
 open Tok (* necessary for camlp5 *)
 
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 7f6270df1a..94eb45fd32 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -29,7 +29,6 @@ open Decl_kinds
 open Constrexpr
 open Redexpr
 open Lemmas
-open Misctypes
 open Locality
 open Vernacinterp
 
@@ -637,7 +636,7 @@ let vernac_scheme l =
 let vernac_combined_scheme lid l =
   if Dumpglob.dump () then
     (Dumpglob.dump_definition lid false "def";
-     List.iter (fun {loc;v=id} -> dump_global (make ?loc @@ Misctypes.AN (make ?loc @@ Ident id))) l);
+     List.iter (fun {loc;v=id} -> dump_global (make ?loc @@ AN (make ?loc @@ Ident id))) l);
  Indschemes.do_combined_scheme lid l
 
 let vernac_universe ~atts l =
diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli
index f6199e8203..3c88a34439 100644
--- a/vernac/vernacentries.mli
+++ b/vernac/vernacentries.mli
@@ -8,9 +8,7 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-open Misctypes
-
-val dump_global : Libnames.reference or_by_notation -> unit
+val dump_global : Libnames.reference Constrexpr.or_by_notation -> unit
 
 (** Vernacular entries *)
 val vernac_require :
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index 9e8dfc4f85..5acac9e255 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -9,7 +9,6 @@
 (************************************************************************)
 
 open Names
-open Misctypes
 open Constrexpr
 open Libnames
 
-- 
cgit v1.2.3