Merge PR #7677: [api] Remove Misctypes

9 files changed, 40 insertions, 18 deletions

diff --git a/engine/evar_kinds.ml b/engine/evar_kinds.ml
index 6e123d6429..12e2fda8e2 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/evarutil.ml b/engine/evarutil.ml
index 648f960354..82be4791fc 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -436,12 +436,12 @@ let new_pure_evar_full evd evi =
   (evd, evk)
 
 let new_pure_evar?(src=default_source) ?(filter = Filter.identity) ?candidates ?(store = Store.empty) ?naming ?(principal=false) sign evd typ =
-  let default_naming = Misctypes.IntroAnonymous in
+  let default_naming = IntroAnonymous in
   let naming = Option.default default_naming naming in
   let name = match naming with
-  | Misctypes.IntroAnonymous -> None
-  | Misctypes.IntroIdentifier id -> Some id
-  | Misctypes.IntroFresh id ->
+  | IntroAnonymous -> None
+  | IntroIdentifier id -> Some id
+  | IntroFresh id ->
     let has_name id = try let _ = Evd.evar_key id evd in true with Not_found -> false in
     let id = Namegen.next_ident_away_from id has_name in
     Some id
diff --git a/engine/evarutil.mli b/engine/evarutil.mli
index f83f262b4a..c17f3d1683 100644
--- a/engine/evarutil.mli
+++ b/engine/evarutil.mli
@@ -12,6 +12,7 @@ open Names
 open Constr
 open Evd
 open Environ
+open Namegen
 open EConstr
 
 (** This module provides useful higher-level functions for evar manipulation. *)
@@ -27,7 +28,7 @@ val mk_new_meta : unit -> constr
 val new_evar_from_context :
   ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t ->
   ?candidates:constr list -> ?store:Store.t ->
-  ?naming:Misctypes.intro_pattern_naming_expr ->
+  ?naming:intro_pattern_naming_expr ->
   ?principal:bool ->
   named_context_val -> evar_map  -> types -> evar_map * EConstr.t
 
@@ -40,14 +41,14 @@ type naming_mode =
 val new_evar :
   ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t ->
   ?candidates:constr list -> ?store:Store.t ->
-  ?naming:Misctypes.intro_pattern_naming_expr ->
+  ?naming:intro_pattern_naming_expr ->
   ?principal:bool -> ?hypnaming:naming_mode ->
   env -> evar_map -> types -> evar_map * EConstr.t
 
 val new_pure_evar :
   ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t ->
   ?candidates:constr list -> ?store:Store.t ->
-  ?naming:Misctypes.intro_pattern_naming_expr ->
+  ?naming:intro_pattern_naming_expr ->
   ?principal:bool ->
   named_context_val -> evar_map -> types -> evar_map * Evar.t
 
@@ -57,7 +58,7 @@ val new_pure_evar_full : evar_map -> evar_info -> evar_map * Evar.t
     them during type-checking and unification. *)
 val new_type_evar :
   ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t ->
-  ?naming:Misctypes.intro_pattern_naming_expr ->
+  ?naming:intro_pattern_naming_expr ->
   ?principal:bool -> ?hypnaming:naming_mode ->
   env -> evar_map -> rigid ->
   evar_map * (constr * Sorts.t)
@@ -79,7 +80,7 @@ val new_global : evar_map -> GlobRef.t -> evar_map * constr
    as a telescope) is [sign] *)
 val new_evar_instance :
   ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> ?candidates:constr list ->
-  ?store:Store.t -> ?naming:Misctypes.intro_pattern_naming_expr ->
+  ?store:Store.t -> ?naming:intro_pattern_naming_expr ->
   ?principal:bool ->
  named_context_val -> evar_map -> types ->
   constr list -> evar_map * constr
@@ -262,13 +263,13 @@ val meta_counter_summary_tag : int Summary.Dyn.tag
 val e_new_evar :
   env -> evar_map ref -> ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t ->
   ?candidates:constr list -> ?store:Store.t ->
-  ?naming:Misctypes.intro_pattern_naming_expr ->
+  ?naming:intro_pattern_naming_expr ->
   ?principal:bool -> ?hypnaming:naming_mode -> types -> constr
 [@@ocaml.deprecated "Use [Evarutil.new_evar]"]
 
 val e_new_type_evar : env -> evar_map ref ->
   ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t ->
-  ?naming:Misctypes.intro_pattern_naming_expr ->
+  ?naming:intro_pattern_naming_expr ->
   ?principal:bool -> ?hypnaming:naming_mode -> rigid -> constr * Sorts.t
 [@@ocaml.deprecated "Use [Evarutil.new_type_evar]"]
 
diff --git a/engine/namegen.ml b/engine/namegen.ml
index c069ec5a06..23c6911396 100644
--- a/engine/namegen.ml
+++ b/engine/namegen.ml
@@ -29,6 +29,18 @@ open Context.Rel.Declaration
 
 module RelDecl = Context.Rel.Declaration
 
+(** General evar naming using intro patterns  *)
+type intro_pattern_naming_expr =
+  | IntroIdentifier of Id.t
+  | IntroFresh of Id.t
+  | IntroAnonymous
+
+let intro_pattern_naming_eq nam1 nam2 = match nam1, nam2 with
+| IntroAnonymous, IntroAnonymous -> true
+| IntroIdentifier id1, IntroIdentifier id2 -> Names.Id.equal id1 id2
+| IntroFresh id1, IntroFresh id2 -> Names.Id.equal id1 id2
+| _ -> false
+
 (**********************************************************************)
 (* Conventional names *)
 
diff --git a/engine/namegen.mli b/engine/namegen.mli
index 1b70ef68dd..a53c3a0d1f 100644
--- a/engine/namegen.mli
+++ b/engine/namegen.mli
@@ -15,6 +15,16 @@ open Environ
 open Evd
 open EConstr
 
+(** General evar naming using intro patterns  *)
+type intro_pattern_naming_expr =
+  | IntroIdentifier of Id.t
+  | IntroFresh of Id.t
+  | IntroAnonymous
+
+(** Equalities on [intro_pattern_naming] *)
+val intro_pattern_naming_eq :
+  intro_pattern_naming_expr -> intro_pattern_naming_expr -> bool
+
 (*********************************************************************
    Conventional default names *)
 
diff --git a/engine/uState.ml b/engine/uState.ml
index 643c621fd5..0e3ecdbf5f 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 e2f25642e5..e7e5b39e09 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 6e59a7c9e6..6ffb4bcf0d 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 e3bc3193d8..c19aa19d50 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]