[api] Misctypes removal: miscellaneous aliases.

8 files changed, 12 insertions, 14 deletions

diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index b5b8697d2..1d1cc62de 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -13,7 +13,6 @@ open Decl_kinds
 open Pretyping
 open Evarutil
 open Evarconv
-open Misctypes
 
 module RelDecl = Context.Rel.Declaration
 
diff --git a/vernac/comFixpoint.mli b/vernac/comFixpoint.mli
index a6992a30b..f51bfbad5 100644
--- a/vernac/comFixpoint.mli
+++ b/vernac/comFixpoint.mli
@@ -33,7 +33,7 @@ val do_cofixpoint :
 type structured_fixpoint_expr = {
   fix_name : Id.t;
   fix_univs : Constrexpr.universe_decl_expr option;
-  fix_annot : Misctypes.lident option;
+  fix_annot : lident option;
   fix_binders : local_binder_expr list;
   fix_body : constr_expr option;
   fix_type : constr_expr
diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml
index e7a308dda..434e836d8 100644
--- a/vernac/egramcoq.ml
+++ b/vernac/egramcoq.ml
@@ -228,7 +228,7 @@ type _ target =
 type prod_info = production_level * production_position
 
 type (_, _) entry =
-| TTName : ('self, Misctypes.lname) entry
+| TTName : ('self, lname) entry
 | TTReference : ('self, reference) entry
 | TTBigint : ('self, Constrexpr.raw_natural_number) entry
 | TTConstr : prod_info * 'r target -> ('r, 'r) entry
diff --git a/vernac/indschemes.mli b/vernac/indschemes.mli
index bd4249cac..261c3d813 100644
--- a/vernac/indschemes.mli
+++ b/vernac/indschemes.mli
@@ -32,17 +32,17 @@ val declare_rewriting_schemes : inductive -> unit
 (** Mutual Minimality/Induction scheme *)
 
 val do_mutual_induction_scheme :
-  (Misctypes.lident * bool * inductive * Sorts.family) list -> unit
+  (lident * bool * inductive * Sorts.family) list -> unit
 
 (** Main calls to interpret the Scheme command *)
 
-val do_scheme : (Misctypes.lident option * scheme) list -> unit
+val do_scheme : (lident option * scheme) list -> unit
 
 (** Combine a list of schemes into a conjunction of them *)
 
 val build_combined_scheme : env -> Constant.t list -> Evd.evar_map * constr * types
 
-val do_combined_scheme : Misctypes.lident -> Misctypes.lident list -> unit
+val do_combined_scheme : lident -> lident list -> unit
 
 (** Hook called at each inductive type definition *)
 
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index 2245e762f..8f64f5519 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -92,7 +92,7 @@ let pr_grammar = function
 (* Parse a format (every terminal starting with a letter or a single
    quote (except a single quote alone) must be quoted) *)
 
-let parse_format ({CAst.loc;v=str} : Misctypes.lstring) =
+let parse_format ({CAst.loc;v=str} : lstring) =
   let len = String.length str in
   (* TODO: update the line of the location when the string contains newlines *)
   let make_loc i j = Option.map (Loc.shift_loc (i+1) (j-len)) loc in
@@ -792,7 +792,7 @@ type notation_modifier = {
   only_parsing  : bool;
   only_printing : bool;
   compat        : Flags.compat_version option;
-  format        : Misctypes.lstring option;
+  format        : lstring option;
   extra         : (string * string) list;
 }
 
@@ -1104,7 +1104,7 @@ module SynData = struct
     only_parsing  : bool;
     only_printing : bool;
     compat        : Flags.compat_version option;
-    format        : Misctypes.lstring option;
+    format        : lstring option;
     extra         : (string * string) list;
 
     (* XXX: Callback to printing, must remove *)
diff --git a/vernac/metasyntax.mli b/vernac/metasyntax.mli
index a6c12e089..f6de75b07 100644
--- a/vernac/metasyntax.mli
+++ b/vernac/metasyntax.mli
@@ -14,7 +14,6 @@ open Notation
 open Constrexpr
 open Notation_term
 open Environ
-open Misctypes
 
 val add_token_obj : string -> unit
 
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 00f1760c2..1ab24b670 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -298,10 +298,10 @@ type obligation =
 type obligations = (obligation array * int)
 
 type fixpoint_kind =
-  | IsFixpoint of (Misctypes.lident option * Constrexpr.recursion_order_expr) list
+  | IsFixpoint of (lident option * Constrexpr.recursion_order_expr) list
   | IsCoFixpoint
 
-type notations = (Misctypes.lstring * Constrexpr.constr_expr * Notation_term.scope_name option) list
+type notations = (lstring * Constrexpr.constr_expr * Notation_term.scope_name option) list
 
 type program_info_aux = {
   prg_name: Id.t;
diff --git a/vernac/obligations.mli b/vernac/obligations.mli
index b1eaf51ac..a37c30aaf 100644
--- a/vernac/obligations.mli
+++ b/vernac/obligations.mli
@@ -62,10 +62,10 @@ val add_definition : Names.Id.t -> ?term:constr -> types ->
   ?hook:(UState.t -> unit) Lemmas.declaration_hook -> ?opaque:bool -> obligation_info -> progress
 
 type notations =
-    (Misctypes.lstring * Constrexpr.constr_expr * Notation_term.scope_name option) list
+    (lstring * Constrexpr.constr_expr * Notation_term.scope_name option) list
 
 type fixpoint_kind =
-  | IsFixpoint of (Misctypes.lident option * Constrexpr.recursion_order_expr) list
+  | IsFixpoint of (lident option * Constrexpr.recursion_order_expr) list
   | IsCoFixpoint
 
 val add_mutual_definitions :