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.
---
 pretyping/locus.ml     |  5 ++++-
 pretyping/locusops.ml  |  4 ++--
 pretyping/misctypes.ml | 28 ----------------------------
 3 files changed, 6 insertions(+), 31 deletions(-)
 delete mode 100644 pretyping/misctypes.ml

(limited to 'pretyping')

diff --git a/pretyping/locus.ml b/pretyping/locus.ml
index 95a2e495be..37dd120c1a 100644
--- a/pretyping/locus.ml
+++ b/pretyping/locus.ml
@@ -9,10 +9,13 @@
 (************************************************************************)
 
 open Names
-open Misctypes
 
 (** Locus : positions in hypotheses and goals *)
 
+type 'a or_var =
+  | ArgArg of 'a
+  | ArgVar of lident
+
 (** {6 Occurrences} *)
 
 type 'a occurrences_gen =
diff --git a/pretyping/locusops.ml b/pretyping/locusops.ml
index 1664e68f2b..6b6a3f8a9f 100644
--- a/pretyping/locusops.ml
+++ b/pretyping/locusops.ml
@@ -86,8 +86,8 @@ let concrete_clause_of enum_hyps cl =
 (** Miscellaneous functions *)
 
 let out_arg = function
-  | Misctypes.ArgVar _ -> CErrors.anomaly (Pp.str "Unevaluated or_var variable.")
-  | Misctypes.ArgArg x -> x
+  | ArgVar _ -> CErrors.anomaly (Pp.str "Unevaluated or_var variable.")
+  | ArgArg x -> x
 
 let occurrences_of_hyp id cls =
   let rec hyp_occ = function
diff --git a/pretyping/misctypes.ml b/pretyping/misctypes.ml
deleted file mode 100644
index 332a901827..0000000000
--- a/pretyping/misctypes.ml
+++ /dev/null
@@ -1,28 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
-(* <O___,, *       (see CREDITS file for the list of authors)           *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-open Names
-
-(** Some utility types for parsing *)
-
-type 'a or_var =
-  | ArgArg of 'a
-  | ArgVar of lident
-
-type 'a and_short_name = 'a * lident option
-
-type 'a or_by_notation_r =
-  | AN of 'a
-  | ByNotation of (string * string option)
-
-type 'a or_by_notation = 'a or_by_notation_r CAst.t
-
-(* NB: the last string in [ByNotation] is actually a [Notation.delimiters],
-   but this formulation avoids a useless dependency. *)
-- 
cgit v1.2.3