[api] Remove Misctypes.

We move the last 3 types to more adequate places.

Author: ejgallego

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

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

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) ->

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

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

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
 

library/library.mllib

@@ -6,7 +6,6 @@ Nametab
 Global
 Decl_kinds
 Lib
-Misctypes
 Declaremods
 Loadpath
 Library

parsing/g_prim.ml4

@@ -85,8 +85,8 @@ GEXTEND Gram
     [ [ s = ne_string; sc = OPT ["%"; key = IDENT -> key ] -> (s, sc) ] ]
   ;
   smart_global:
-    [ [ c = reference -> CAst.make ~loc:!@loc @@ Misctypes.AN c
-      | ntn = by_notation -> CAst.make ~loc:!@loc @@ Misctypes.ByNotation ntn ] ]
+    [ [ c = reference -> CAst.make ~loc:!@loc @@ Constrexpr.AN c
+      | ntn = by_notation -> CAst.make ~loc:!@loc @@ Constrexpr.ByNotation ntn ] ]
   ;
   qualid:
     [ [ qid = basequalid -> CAst.make ~loc:!@loc qid ] ]

parsing/pcoq.mli

@@ -13,7 +13,6 @@ open Extend
 open Genarg
 open Constrexpr
 open Libnames
-open Misctypes
 
 (** The parser of Coq *)
 

plugins/extraction/extract_env.ml

@@ -646,7 +646,7 @@ let separate_extraction lr =
     is \verb!Extraction! [qualid]. *)
 
 let simple_extraction r =
-  Vernacentries.dump_global CAst.(make (Misctypes.AN r));
+  Vernacentries.dump_global CAst.(make (Constrexpr.AN r));
   match locate_ref [r] with
   | ([], [mp]) as p -> full_extr None p
   | [r],[] ->