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

We move the last 3 types to more adequate places.
---
 interp/constrexpr.ml   | 9 +++++++++
 interp/genredexpr.ml   | 1 -
 interp/smartlocate.ml  | 5 ++---
 interp/smartlocate.mli | 5 ++---
 interp/stdarg.ml       | 2 ++
 interp/stdarg.mli      | 4 +++-
 6 files changed, 18 insertions(+), 8 deletions(-)

(limited to 'interp')

diff --git a/interp/constrexpr.ml b/interp/constrexpr.ml
index 60f2c683a..d725f5afa 100644
--- a/interp/constrexpr.ml
+++ b/interp/constrexpr.ml
@@ -22,6 +22,15 @@ type name_decl = lname * universe_decl_expr option
 
 type notation = string
 
+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. *)
+
 type explicitation =
   | ExplByPos of int * Id.t option (* a reference to the n-th product starting from left *)
   | ExplByName of Id.t
diff --git a/interp/genredexpr.ml b/interp/genredexpr.ml
index 983493b25..42c1fe429 100644
--- a/interp/genredexpr.ml
+++ b/interp/genredexpr.ml
@@ -57,7 +57,6 @@ type ('a,'b,'c) may_eval =
 
 open Libnames
 open Constrexpr
-open Misctypes
 
 type r_trm = constr_expr
 type r_pat = constr_pattern_expr
diff --git a/interp/smartlocate.ml b/interp/smartlocate.ml
index 1f4a93a6f..e1fbdba87 100644
--- a/interp/smartlocate.ml
+++ b/interp/smartlocate.ml
@@ -18,7 +18,6 @@ open Pp
 open CErrors
 open Libnames
 open Globnames
-open Misctypes
 open Syntax_def
 open Notation_term
 
@@ -65,13 +64,13 @@ let global_with_alias ?head r =
   try locate_global_with_alias ?head qid
   with Not_found -> Nametab.error_global_not_found qid
 
-let smart_global ?head = CAst.with_loc_val (fun ?loc -> function
+let smart_global ?head = let open Constrexpr in CAst.with_loc_val (fun ?loc -> function
   | AN r ->
     global_with_alias ?head r
   | ByNotation (ntn,sc) ->
     Notation.interp_notation_as_global_reference ?loc (fun _ -> true) ntn sc)
 
-let smart_global_inductive = CAst.with_loc_val (fun ?loc -> function
+let smart_global_inductive = let open Constrexpr in CAst.with_loc_val (fun ?loc -> function
   | AN r ->
     global_inductive_with_alias r
   | ByNotation (ntn,sc) ->
diff --git a/interp/smartlocate.mli b/interp/smartlocate.mli
index 45037b8b3..6b574d7b5 100644
--- a/interp/smartlocate.mli
+++ b/interp/smartlocate.mli
@@ -11,7 +11,6 @@
 open Names
 open Libnames
 open Globnames
-open Misctypes
 
 (** [locate_global_with_alias] locates global reference possibly following
    a notation if this notation has a role of aliasing; raise [Not_found]
@@ -33,7 +32,7 @@ val global_with_alias : ?head:bool -> reference -> GlobRef.t
 val global_inductive_with_alias : reference -> inductive
 
 (** Locate a reference taking into account notations and "aliases" *)
-val smart_global : ?head:bool -> reference or_by_notation -> GlobRef.t
+val smart_global : ?head:bool -> reference Constrexpr.or_by_notation -> GlobRef.t
 
 (** The same for inductive types *)
-val smart_global_inductive : reference or_by_notation -> inductive
+val smart_global_inductive : reference Constrexpr.or_by_notation -> inductive
diff --git a/interp/stdarg.ml b/interp/stdarg.ml
index 7a7bb9a84..7b01b6dc1 100644
--- a/interp/stdarg.ml
+++ b/interp/stdarg.ml
@@ -11,6 +11,8 @@
 open Genarg
 open Geninterp
 
+type 'a and_short_name = 'a * Names.lident option
+
 let make0 ?dyn name =
   let wit = Genarg.make0 name in
   let () = register_val0 wit dyn in
diff --git a/interp/stdarg.mli b/interp/stdarg.mli
index 4159e6054..4792cda08 100644
--- a/interp/stdarg.mli
+++ b/interp/stdarg.mli
@@ -17,9 +17,11 @@ open Libnames
 open Genredexpr
 open Pattern
 open Constrexpr
-open Misctypes
 open Genarg
 open Genintern
+open Locus
+
+type 'a and_short_name = 'a * lident option
 
 val wit_unit : unit uniform_genarg_type
 
-- 
cgit v1.2.3