[api] Misctypes removal: miscellaneous aliases.

39 files changed, 66 insertions, 68 deletions

diff --git a/engine/evar_kinds.ml b/engine/evar_kinds.ml
index 6e123d642..12e2fda8e 100644
--- a/engine/evar_kinds.ml
+++ b/engine/evar_kinds.ml
@@ -9,7 +9,6 @@
 (************************************************************************)
 
 open Names
-open Misctypes
 
 (** The kinds of existential variable *)
 
@@ -18,7 +17,7 @@ open Misctypes
 
 type obligation_definition_status = Define of bool | Expand
 
-type matching_var_kind = FirstOrderPatVar of patvar | SecondOrderPatVar of patvar
+type matching_var_kind = FirstOrderPatVar of Id.t | SecondOrderPatVar of Id.t
 
 type subevar_kind = Domain | Codomain | Body
 
diff --git a/engine/uState.ml b/engine/uState.ml
index 643c621fd..0e3ecdbf5 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -312,7 +312,7 @@ type ('a, 'b) gen_universe_decl = {
   univdecl_extensible_constraints : bool (* Can new constraints be added *) }
 
 type universe_decl =
-  (Misctypes.lident list, Univ.Constraint.t) gen_universe_decl
+  (lident list, Univ.Constraint.t) gen_universe_decl
 
 let default_univ_decl =
   { univdecl_instance = [];
diff --git a/engine/uState.mli b/engine/uState.mli
index e2f25642e..e7e5b39e0 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -26,7 +26,7 @@ val empty : t
 
 val make : UGraph.t -> t
 
-val make_with_initial_binders : UGraph.t -> Misctypes.lident list -> t
+val make_with_initial_binders : UGraph.t -> lident list -> t
 
 val is_empty : t -> bool
 
@@ -145,7 +145,7 @@ type ('a, 'b) gen_universe_decl = {
   univdecl_extensible_constraints : bool (* Can new constraints be added *) }
 
 type universe_decl =
-  (Misctypes.lident list, Univ.Constraint.t) gen_universe_decl
+  (lident list, Univ.Constraint.t) gen_universe_decl
 
 val default_univ_decl : universe_decl
 
diff --git a/engine/univNames.ml b/engine/univNames.ml
index 6e59a7c9e..6ffb4bcf0 100644
--- a/engine/univNames.ml
+++ b/engine/univNames.ml
@@ -89,7 +89,7 @@ let register_universe_binders ref ubinders =
   if not (Id.Map.is_empty ubinders)
   then Lib.add_anonymous_leaf (ubinder_obj (ref,ubinders))
 
-type univ_name_list = Misctypes.lname list
+type univ_name_list = Names.lname list
 
 let universe_binders_with_opt_names ref levels = function
   | None -> universe_binders_of_global ref
diff --git a/engine/univNames.mli b/engine/univNames.mli
index e3bc3193d..c19aa19d5 100644
--- a/engine/univNames.mli
+++ b/engine/univNames.mli
@@ -29,7 +29,7 @@ val empty_binders : universe_binders
 val register_universe_binders : Names.GlobRef.t -> universe_binders -> unit
 val universe_binders_of_global : Names.GlobRef.t -> universe_binders
 
-type univ_name_list = Misctypes.lname list
+type univ_name_list = Names.lname list
 
 (** [universe_binders_with_opt_names ref u l]
 
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
diff --git a/kernel/names.ml b/kernel/names.ml
index 54f089e60..597061278 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -852,3 +852,9 @@ let eq_egr e1 e2 = match e1, e2 with
     EvalConstRef con1, EvalConstRef con2 -> Constant.equal con1 con2
   | EvalVarRef id1, EvalVarRef id2 -> Id.equal id1 id2
   | _, _ -> false
+
+(** Located identifiers and objects with syntax. *)
+
+type lident = Id.t CAst.t
+type lname = Name.t CAst.t
+type lstring = string CAst.t
diff --git a/kernel/names.mli b/kernel/names.mli
index f988b559a..4eb5adb62 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -605,3 +605,9 @@ type evaluable_global_reference =
   | EvalConstRef of Constant.t
 
 val eq_egr : evaluable_global_reference ->  evaluable_global_reference -> bool
+
+(** Located identifiers and objects with syntax. *)
+
+type lident = Id.t CAst.t
+type lname = Name.t CAst.t
+type lstring = string CAst.t
diff --git a/library/declaremods.ml b/library/declaremods.ml
index e8d89f96b..0b3b461e6 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -17,7 +17,6 @@ open Entries
 open Libnames
 open Libobject
 open Mod_subst
-open Misctypes
 
 (** {6 Inlining levels} *)
 
diff --git a/library/declaremods.mli b/library/declaremods.mli
index 63b25c7e4..b42a59bfb 100644
--- a/library/declaremods.mli
+++ b/library/declaremods.mli
@@ -36,7 +36,7 @@ type 'modast module_interpretor =
     Entries.module_struct_entry * module_kind * Univ.ContextSet.t
 
 type 'modast module_params =
-  (Misctypes.lident list * ('modast * inline)) list
+  (lident list * ('modast * inline)) list
 
 (** [declare_module interp_modast id fargs typ exprs]
    declares module [id], with structure constructed by [interp_modast]
diff --git a/library/misctypes.ml b/library/misctypes.ml
index a12caef80..3b629f449 100644
--- a/library/misctypes.ml
+++ b/library/misctypes.ml
@@ -10,18 +10,6 @@
 
 open Names
 
-(** Basic types used both in [constr_expr], [glob_constr], and [vernacexpr] *)
-
-(** Located identifiers and objects with syntax. *)
-
-type lident = Id.t CAst.t
-type lname = Name.t CAst.t
-type lstring = string CAst.t
-
-(** Cases pattern variables *)
-
-type patvar = Id.t
-
 (** Introduction patterns *)
 
 type 'constr intro_pattern_expr =
diff --git a/plugins/ltac/g_tactic.ml4 b/plugins/ltac/g_tactic.ml4
index 15db4ca6a..038d55e4b 100644
--- a/plugins/ltac/g_tactic.ml4
+++ b/plugins/ltac/g_tactic.ml4
@@ -11,6 +11,7 @@
 open Pp
 open CErrors
 open Util
+open Names
 open Tacexpr
 open Genredexpr
 open Constrexpr
@@ -383,19 +384,19 @@ GEXTEND Gram
   ;
   hypident:
     [ [ id = id_or_meta ->
-        let id : Misctypes.lident = id in
+        let id : lident = id in
         id,InHyp
       | "("; IDENT "type"; IDENT "of"; id = id_or_meta; ")" ->
-        let id : Misctypes.lident = id in
+        let id : lident = id in
         id,InHypTypeOnly
       | "("; IDENT "value"; IDENT "of"; id = id_or_meta; ")" ->
-        let id : Misctypes.lident = id in
+        let id : lident = id in
         id,InHypValueOnly
     ] ]
   ;
   hypident_occ:
     [ [ (id,l)=hypident; occs=occs ->
-        let id : Misctypes.lident = id in
+        let id : lident = id in
         ((occs,id),l) ] ]
   ;
   in_clause:
diff --git a/plugins/ltac/pltac.mli b/plugins/ltac/pltac.mli
index 434feba95..de23d2f8e 100644
--- a/plugins/ltac/pltac.mli
+++ b/plugins/ltac/pltac.mli
@@ -20,7 +20,7 @@ open Misctypes
 val open_constr : constr_expr Gram.entry
 val constr_with_bindings : constr_expr with_bindings Gram.entry
 val bindings : constr_expr bindings Gram.entry
-val hypident : (lident * Locus.hyp_location_flag) Gram.entry
+val hypident : (Names.lident * Locus.hyp_location_flag) Gram.entry
 val constr_may_eval : (constr_expr,reference or_by_notation,constr_expr) may_eval Gram.entry
 val constr_eval : (constr_expr,reference or_by_notation,constr_expr) may_eval Gram.entry
 val uconstr : constr_expr Gram.entry
@@ -29,8 +29,8 @@ val destruction_arg : constr_expr with_bindings Tactics.destruction_arg Gram.ent
 val int_or_var : int or_var Gram.entry
 val simple_tactic : raw_tactic_expr Gram.entry
 val simple_intropattern : constr_expr intro_pattern_expr CAst.t Gram.entry
-val in_clause : lident Locus.clause_expr Gram.entry
-val clause_dft_concl : lident Locus.clause_expr Gram.entry
+val in_clause : Names.lident Locus.clause_expr Gram.entry
+val clause_dft_concl : Names.lident Locus.clause_expr Gram.entry
 val tactic_arg : raw_tactic_arg Gram.entry
 val tactic_expr : raw_tactic_expr Gram.entry
 val binder_tactic : raw_tactic_expr Gram.entry
diff --git a/plugins/ltac/tactic_debug.mli b/plugins/ltac/tactic_debug.mli
index 734e76b56..175341df0 100644
--- a/plugins/ltac/tactic_debug.mli
+++ b/plugins/ltac/tactic_debug.mli
@@ -76,7 +76,7 @@ val db_logic_failure : debug_info -> exn -> unit Proofview.NonLogical.t
 
 (** Prints a logic failure message for a rule *)
 val db_breakpoint : debug_info ->
-  Misctypes.lident message_token list -> unit Proofview.NonLogical.t
+  lident message_token list -> unit Proofview.NonLogical.t
 
 val extract_ltac_trace :
   ?loc:Loc.t -> Tacexpr.ltac_trace -> Pp.t option Loc.located
diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml
index 996a2dc36..519a5466b 100644
--- a/pretyping/pattern.ml
+++ b/pretyping/pattern.ml
@@ -13,6 +13,9 @@ open Misctypes
 
 (** {5 Patterns} *)
 
+(** Cases pattern variables *)
+type patvar = Id.t
+
 type case_info_pattern =
     { cip_style : Constr.case_style;
       cip_ind : inductive option;
diff --git a/pretyping/patternops.mli b/pretyping/patternops.mli
index dfbfb147f..36317b3ac 100644
--- a/pretyping/patternops.mli
+++ b/pretyping/patternops.mli
@@ -10,7 +10,6 @@
 
 open Names
 open Mod_subst
-open Misctypes
 open Glob_term
 open Pattern
 open EConstr
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 70588b6ad..d3aa7ac64 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -30,7 +30,7 @@ type 'a hint_info_gen =
     { hint_priority : int option;
       hint_pattern : 'a option }
 
-type hint_info = (Misctypes.patvar list * Pattern.constr_pattern) hint_info_gen
+type hint_info = (Pattern.patvar list * Pattern.constr_pattern) hint_info_gen
 
 let typeclasses_unique_solutions = ref false
 let set_typeclasses_unique_solutions d = (:=) typeclasses_unique_solutions d
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index c78382c82..e4a56960c 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -21,7 +21,7 @@ type 'a hint_info_gen =
     { hint_priority : int option;
       hint_pattern : 'a option }
 
-type hint_info = (Misctypes.patvar list * Pattern.constr_pattern) hint_info_gen
+type hint_info = (Pattern.patvar list * Pattern.constr_pattern) hint_info_gen
 
 (** This module defines type-classes *)
 type typeclass = {
diff --git a/pretyping/typeclasses_errors.ml b/pretyping/typeclasses_errors.ml
index a1ac53c73..2720a3e4d 100644
--- a/pretyping/typeclasses_errors.ml
+++ b/pretyping/typeclasses_errors.ml
@@ -18,7 +18,7 @@ type contexts = Parameters | Properties
 
 type typeclass_error =
     | NotAClass of constr
-    | UnboundMethod of GlobRef.t * Misctypes.lident (* Class name, method *)
+    | UnboundMethod of GlobRef.t * lident (* Class name, method *)
 
 exception TypeClassError of env * typeclass_error
 
diff --git a/pretyping/typeclasses_errors.mli b/pretyping/typeclasses_errors.mli
index 1003f2ae1..9831627a9 100644
--- a/pretyping/typeclasses_errors.mli
+++ b/pretyping/typeclasses_errors.mli
@@ -16,11 +16,11 @@ type contexts = Parameters | Properties
 
 type typeclass_error =
   | NotAClass of constr
-  | UnboundMethod of GlobRef.t * Misctypes.lident (** Class name, method *)
+  | UnboundMethod of GlobRef.t * lident (** Class name, method *)
 
 exception TypeClassError of env * typeclass_error
 
 val not_a_class : env -> constr -> 'a
 
-val unbound_method : env -> GlobRef.t -> Misctypes.lident -> 'a
+val unbound_method : env -> GlobRef.t -> lident -> 'a
 
diff --git a/printing/ppconstr.mli b/printing/ppconstr.mli
index 05f48ec79..89df8f5b9 100644
--- a/printing/ppconstr.mli
+++ b/printing/ppconstr.mli
@@ -39,7 +39,7 @@ val pr_name : Name.t -> Pp.t
 [@@ocaml.deprecated "alias of Names.Name.print"]
 
 val pr_qualid : qualid -> Pp.t
-val pr_patvar : patvar -> Pp.t
+val pr_patvar : Pattern.patvar -> Pp.t
 
 val pr_glob_level : Glob_term.glob_level -> Pp.t
 val pr_glob_sort : Glob_term.glob_sort -> Pp.t
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 946379356..3120c97b5 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -83,7 +83,7 @@ type opacity_flag = Opaque | Transparent
 type proof_ending =
   | Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry * UState.t
   | Proved of opacity_flag *
-              Misctypes.lident option *
+              lident option *
               proof_object
 
 type proof_terminator = proof_ending -> unit
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index 0141cacb9..9e07ed2d0 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -22,7 +22,7 @@ val check_no_pending_proof : unit -> unit
 val get_current_proof_name : unit -> Names.Id.t
 val get_all_proof_names : unit -> Names.Id.t list
 
-val discard : Misctypes.lident -> unit
+val discard : Names.lident -> unit
 val discard_current : unit -> unit
 val discard_all : unit -> unit
 
@@ -54,7 +54,7 @@ type proof_ending =
   | Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry *
                 UState.t
   | Proved of opacity_flag *
-              Misctypes.lident option *
+              Names.lident option *
               proof_object
 type proof_terminator
 type closed_proof = proof_object * proof_terminator
@@ -126,7 +126,7 @@ val set_endline_tactic : Genarg.glob_generic_argument -> unit
  * (w.r.t. type dependencies and let-ins covered by it) + a list of
  * ids to be cleared *)
 val set_used_variables :
-  Names.Id.t list -> Context.Named.t * Misctypes.lident list
+  Names.Id.t list -> Context.Named.t * Names.lident list
 val get_used_variables : unit -> Context.Named.t option
 
 (** Get the universe declaration associated to the current proof. *)
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 :