[api] Misctypes removal: miscellaneous aliases.

9 files changed, 13 insertions, 14 deletions

diff --git a/interp/constrexpr.ml b/interp/constrexpr.ml
index ca6ea94f0..d6b395e01 100644
--- a/interp/constrexpr.ml
+++ b/interp/constrexpr.ml
@@ -95,7 +95,7 @@ and constr_expr_r =
   | CIf of constr_expr * (lname option * constr_expr option)
          * constr_expr * constr_expr
   | CHole   of Evar_kinds.t option * intro_pattern_naming_expr * Genarg.raw_generic_argument option
-  | CPatVar of patvar
+  | CPatVar of Pattern.patvar
   | CEvar   of Glob_term.existential_name * (Id.t * constr_expr) list
   | CSort   of Glob_term.glob_sort
   | CCast   of constr_expr * constr_expr cast_type
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index e09b7a793..057e10c00 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -606,7 +606,7 @@ let traverse_binder intern_pat ntnvars (terms,_,binders,_ as subst) avoid (renam
     (renaming',env), None, Name id'
 
 type binder_action =
-| AddLetIn of Misctypes.lname * constr_expr * constr_expr option
+| AddLetIn of lname * constr_expr * constr_expr option
 | AddTermIter of (constr_expr * subscopes) Names.Id.Map.t
 | AddPreBinderIter of Id.t * local_binder_expr (* A binder to be internalized *)
 | AddBinderIter of Id.t * extended_glob_local_binder (* A binder already internalized - used for generalized binders *)
@@ -1073,11 +1073,11 @@ let interp_reference vars r =
 
 (** Private internalization patterns *)
 type 'a raw_cases_pattern_expr_r =
-  | RCPatAlias of 'a raw_cases_pattern_expr * Misctypes.lname
+  | RCPatAlias of 'a raw_cases_pattern_expr * lname
   | RCPatCstr  of GlobRef.t
     * 'a raw_cases_pattern_expr list * 'a raw_cases_pattern_expr list
   (** [RCPatCstr (loc, c, l1, l2)] represents [((@ c l1) l2)] *)
-  | RCPatAtom  of (Misctypes.lident * (Notation_term.tmp_scope_name option * Notation_term.scope_name list)) option
+  | RCPatAtom  of (lident * (Notation_term.tmp_scope_name option * Notation_term.scope_name list)) option
   | RCPatOr    of 'a raw_cases_pattern_expr list
 and 'a raw_cases_pattern_expr = ('a raw_cases_pattern_expr_r, 'a) DAst.t
 
@@ -1385,7 +1385,7 @@ let sort_fields ~complete loc fields completer =
 (** {6 Manage multiple aliases} *)
 
 type alias = {
-  alias_ids : Misctypes.lident list;
+  alias_ids : lident list;
   alias_map : Id.t Id.Map.t;
 }
 
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 4dd719e1f..12f77af30 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -11,7 +11,6 @@
 open Names
 open Evd
 open Environ
-open Misctypes
 open Libnames
 open Glob_term
 open Pattern
diff --git a/interp/declare.mli b/interp/declare.mli
index 4a9f54278..02e73cd66 100644
--- a/interp/declare.mli
+++ b/interp/declare.mli
@@ -87,6 +87,6 @@ val declare_univ_binders : GlobRef.t -> UnivNames.universe_binders -> unit
 
 val declare_universe_context : polymorphic -> Univ.ContextSet.t -> unit
 
-val do_universe : polymorphic -> Misctypes.lident list -> unit
+val do_universe : polymorphic -> lident list -> unit
 val do_constraint : polymorphic -> (Glob_term.glob_level * Univ.constraint_type * Glob_term.glob_level) list ->
                     unit
diff --git a/interp/dumpglob.mli b/interp/dumpglob.mli
index bf83d2df4..931d05a97 100644
--- a/interp/dumpglob.mli
+++ b/interp/dumpglob.mli
@@ -27,7 +27,7 @@ val continue : unit -> unit
 val add_glob : ?loc:Loc.t -> Names.GlobRef.t -> unit
 val add_glob_kn : ?loc:Loc.t -> Names.KerName.t -> unit
 
-val dump_definition : Misctypes.lident -> bool -> string -> unit
+val dump_definition : Names.lident -> bool -> string -> unit
 val dump_moddef : ?loc:Loc.t -> Names.ModPath.t -> string -> unit
 val dump_modref  : ?loc:Loc.t -> Names.ModPath.t -> string -> unit
 val dump_reference  : ?loc:Loc.t -> string -> string -> string -> unit
@@ -39,7 +39,7 @@ val dump_notation :
   (Constrexpr.notation * Notation.notation_location) Loc.located ->
   Notation_term.scope_name option -> bool -> unit
 
-val dump_constraint : Misctypes.lname -> bool -> string -> unit
+val dump_constraint : Names.lname -> bool -> string -> unit
 
 val dump_string : string -> unit
 
diff --git a/interp/genredexpr.ml b/interp/genredexpr.ml
index 80697461a..983493b25 100644
--- a/interp/genredexpr.ml
+++ b/interp/genredexpr.ml
@@ -52,7 +52,7 @@ type ('a,'b,'c) red_expr_gen =
 type ('a,'b,'c) may_eval =
   | ConstrTerm of 'a
   | ConstrEval of ('a,'b,'c) red_expr_gen * 'a
-  | ConstrContext of Misctypes.lident * 'a
+  | ConstrContext of Names.lident * 'a
   | ConstrTypeOf of 'a
 
 open Libnames
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index b48db9ac5..b54e2badd 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -53,7 +53,7 @@ let cache_generalizable_type (_,(local,cmd)) =
 let load_generalizable_type _ (_,(local,cmd)) =
   generalizable_table := add_generalizable cmd !generalizable_table
 
-let in_generalizable : bool * Misctypes.lident list option -> obj =
+let in_generalizable : bool * lident list option -> obj =
   declare_object {(default_object "GENERALIZED-IDENT") with
     load_function = load_generalizable_type;
     cache_function = cache_generalizable_type;
diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli
index e64c5c542..25394fc0d 100644
--- a/interp/implicit_quantifiers.mli
+++ b/interp/implicit_quantifiers.mli
@@ -13,7 +13,7 @@ open Glob_term
 open Constrexpr
 open Libnames
 
-val declare_generalizable : local:bool -> Misctypes.lident list option -> unit
+val declare_generalizable : local:bool -> lident list option -> unit
 
 val ids_of_list : Id.t list -> Id.Set.t
 val destClassApp : constr_expr -> (reference * constr_expr list * instance_expr option) CAst.t
@@ -31,7 +31,7 @@ val free_vars_of_binders :
    order with the location of their first occurrence *)
 
 val generalizable_vars_of_glob_constr : ?bound:Id.Set.t -> ?allowed:Id.Set.t ->
-  glob_constr -> Misctypes.lident list
+  glob_constr -> lident list
 
 val make_fresh : Id.Set.t -> Environ.env -> Id.t -> Id.t
 
diff --git a/interp/reserve.mli b/interp/reserve.mli
index daee58639..a10858e71 100644
--- a/interp/reserve.mli
+++ b/interp/reserve.mli
@@ -11,5 +11,5 @@
 open Names
 open Notation_term
 
-val declare_reserved_type : Misctypes.lident list -> notation_constr -> unit
+val declare_reserved_type : lident list -> notation_constr -> unit
 val find_reserved_type : Id.t -> notation_constr