Merge PR #7677: [api] Remove Misctypes

165 files changed, 670 insertions, 655 deletions

diff --git a/dev/base_include b/dev/base_include
index fc38305cc..574bc097e 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -108,8 +108,6 @@ open Inductiveops
 open Locusops
 open Find_subterm
 open Unification
-open Miscops
-open Miscops
 open Nativenorm
 open Typeclasses
 open Typeclasses_errors
diff --git a/dev/ci/user-overlays/07677-ejgallego-misctypes+bye2.sh b/dev/ci/user-overlays/07677-ejgallego-misctypes+bye2.sh
new file mode 100644
index 000000000..b4f716139
--- /dev/null
+++ b/dev/ci/user-overlays/07677-ejgallego-misctypes+bye2.sh
@@ -0,0 +1,8 @@
+_OVERLAY_BRANCH=misctypes+bye2
+
+if [ "$CI_PULL_REQUEST" = "7677" ] || [ "$CI_BRANCH" = "_OVERLAY_BRANCH" ]; then
+
+    Equations_CI_BRANCH="$_OVERLAY_BRANCH"
+    Equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations
+
+fi
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/evarutil.ml b/engine/evarutil.ml
index 648f96035..82be4791f 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 f83f262b4..c17f3d168 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 c069ec5a0..23c691139 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 1b70ef68d..a53c3a0d1 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 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..d725f5afa 100644
--- a/interp/constrexpr.ml
+++ b/interp/constrexpr.ml
@@ -10,7 +10,6 @@
 
 open Names
 open Libnames
-open Misctypes
 open Decl_kinds
 
 (** {6 Concrete syntax for terms } *)
@@ -23,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
@@ -94,11 +102,11 @@ and constr_expr_r =
                  constr_expr * constr_expr
   | 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
+  | CHole   of Evar_kinds.t option * Namegen.intro_pattern_naming_expr * Genarg.raw_generic_argument option
+  | 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
+  | CCast   of constr_expr * constr_expr Glob_term.cast_type
   | CNotation of notation * constr_notation_substitution
   | CGeneralization of binding_kind * abstraction_kind option * constr_expr
   | CPrim of prim_token
diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index 1be1dd96c..d626630ef 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -14,8 +14,9 @@ open CAst
 open Names
 open Nameops
 open Libnames
+open Namegen
+open Glob_term
 open Constrexpr
-open Misctypes
 open Decl_kinds
 
 (***********************)
@@ -161,7 +162,7 @@ let rec constr_expr_eq e1 e2 =
     | CEvar (id1, c1), CEvar (id2, c2) ->
       Id.equal id1 id2 && List.equal instance_eq c1 c2
     | CSort s1, CSort s2 ->
-      Miscops.glob_sort_eq s1 s2
+      Glob_ops.glob_sort_eq s1 s2
   | CCast(t1,c1), CCast(t2,c2) ->
     constr_expr_eq t1 t2 && cast_expr_eq c1 c2
     | CNotation(n1, s1), CNotation(n2, s2) ->
@@ -395,7 +396,7 @@ let map_constr_expr_with_binders g f e = CAst.map (function
       let (e,bl) = map_local_binders f g e bl in CLambdaN (bl,f e b)
     | CLetIn (na,a,t,b) ->
       CLetIn (na,f e a,Option.map (f e) t,f (Name.fold_right g (na.CAst.v) e) b)
-    | CCast (a,c) -> CCast (f e a, Miscops.map_cast_type (f e) c)
+    | CCast (a,c) -> CCast (f e a, Glob_ops.map_cast_type (f e) c)
     | CNotation (n,(l,ll,bl,bll)) ->
       (* This is an approximation because we don't know what binds what *)
       CNotation (n,(List.map (f e) l,List.map (List.map (f e)) ll, bl,
@@ -545,7 +546,7 @@ let coerce_to_id = function
 
 let coerce_to_name = function
   | { CAst.loc; v = CRef ({v=Ident id},None) } -> CAst.make ?loc @@ Name id
-  | { CAst.loc; v = CHole (None,Misctypes.IntroAnonymous,None) } -> CAst.make ?loc Anonymous
+  | { CAst.loc; v = CHole (None,IntroAnonymous,None) } -> CAst.make ?loc Anonymous
   | { CAst.loc; _ } -> CErrors.user_err ?loc ~hdr:"coerce_to_name"
                          (str "This expression should be a name.")
 
@@ -569,7 +570,7 @@ let mkAppPattern ?loc p lp =
 let rec coerce_to_cases_pattern_expr c = CAst.map_with_loc (fun ?loc -> function
   | CRef (r,None) ->
      CPatAtom (Some r)
-  | CHole (None,Misctypes.IntroAnonymous,None) ->
+  | CHole (None,IntroAnonymous,None) ->
      CPatAtom None
   | CLetIn ({CAst.loc;v=Name id},b,None,{ CAst.v = CRef ({v=Ident id'},None) }) when Id.equal id id' ->
       CPatAlias (coerce_to_cases_pattern_expr b, CAst.(make ?loc @@ Name id))
diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli
index b4f0886ac..1c2348457 100644
--- a/interp/constrexpr_ops.mli
+++ b/interp/constrexpr_ops.mli
@@ -10,7 +10,6 @@
 
 open Names
 open Libnames
-open Misctypes
 open Constrexpr
 
 (** Constrexpr_ops: utilities on [constr_expr] *)
@@ -44,7 +43,7 @@ val local_binders_loc : local_binder_expr list -> Loc.t option
 val mkIdentC : Id.t -> constr_expr
 val mkRefC : reference -> constr_expr
 val mkAppC : constr_expr * constr_expr list -> constr_expr
-val mkCastC : constr_expr * constr_expr cast_type -> constr_expr
+val mkCastC : constr_expr * constr_expr Glob_term.cast_type -> constr_expr
 val mkLambdaC : lname list * binder_kind * constr_expr * constr_expr -> constr_expr
 val mkLetInC : lname * constr_expr * constr_expr option * constr_expr -> constr_expr
 val mkProdC : lname list * binder_kind * constr_expr * constr_expr -> constr_expr
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 86f6ce9ae..c613effcd 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -17,6 +17,7 @@ open Nameops
 open Termops
 open Libnames
 open Globnames
+open Namegen
 open Impargs
 open CAst
 open Constrexpr
@@ -719,7 +720,7 @@ let extended_glob_local_binder_of_decl loc = function
   | (p,bk,None,t) -> GLocalAssum (p,bk,t)
   | (p,bk,Some x, t) ->
     match DAst.get t with
-    | GHole (_, Misctypes.IntroAnonymous, None) -> GLocalDef (p,bk,x,None)
+    | GHole (_, IntroAnonymous, None) -> GLocalDef (p,bk,x,None)
     | _ -> GLocalDef (p,bk,x,Some t)
 
 let extended_glob_local_binder_of_decl ?loc u = DAst.make ?loc (extended_glob_local_binder_of_decl loc u)
@@ -754,13 +755,13 @@ let rec extern inctx scopes vars r =
 
   | GVar id -> CRef (make ?loc @@ Ident id,None)
 
-  | GEvar (n,[]) when !print_meta_as_hole -> CHole (None, Misctypes.IntroAnonymous, None)
+  | GEvar (n,[]) when !print_meta_as_hole -> CHole (None, IntroAnonymous, None)
 
   | GEvar (n,l) ->
       extern_evar n (List.map (on_snd (extern false scopes vars)) l)
 
   | GPatVar kind ->
-      if !print_meta_as_hole then CHole (None, Misctypes.IntroAnonymous, None) else
+      if !print_meta_as_hole then CHole (None, IntroAnonymous, None) else
        (match kind with
          | Evar_kinds.SecondOrderPatVar n -> CPatVar n
          | Evar_kinds.FirstOrderPatVar n -> CEvar (n,[]))
@@ -916,7 +917,7 @@ let rec extern inctx scopes vars r =
 
   | GCast (c, c') ->
       CCast (sub_extern true scopes vars c,
-	     Miscops.map_cast_type (extern_typ scopes vars) c')
+             map_cast_type (extern_typ scopes vars) c')
   | GProj (p, c) ->
     let pr = extern_reference ?loc Id.Set.empty (ConstRef (Projection.constant p)) in
     CProj (pr, sub_extern inctx scopes vars c)
@@ -1159,7 +1160,7 @@ let extern_closed_glob ?lax goal_concl_style env sigma t =
 
 let any_any_branch =
   (* | _ => _ *)
-  CAst.make ([],[DAst.make @@ PatVar Anonymous], DAst.make @@ GHole (Evar_kinds.InternalHole,Misctypes.IntroAnonymous,None))
+  CAst.make ([],[DAst.make @@ PatVar Anonymous], DAst.make @@ GHole (Evar_kinds.InternalHole,IntroAnonymous,None))
 
 let compute_displayed_name_in_pattern sigma avoid na c =
   let open Namegen in
@@ -1183,7 +1184,7 @@ let rec glob_of_pat avoid env sigma pat = DAst.make @@ match pat with
 	    anomaly ~label:"glob_constr_of_pattern" (Pp.str "index to an anonymous variable.")
       with Not_found -> Id.of_string ("_UNBOUND_REL_"^(string_of_int n)) in
       GVar id
-  | PMeta None -> GHole (Evar_kinds.InternalHole, Misctypes.IntroAnonymous,None)
+  | PMeta None -> GHole (Evar_kinds.InternalHole, IntroAnonymous,None)
   | PMeta (Some n) -> GPatVar (Evar_kinds.FirstOrderPatVar n)
   | PProj (p,c) -> GApp (DAst.make @@ GRef (ConstRef (Projection.constant p),None),
 			 [glob_of_pat avoid env sigma c])
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index e09b7a793..d7345b701 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -14,8 +14,8 @@ open Util
 open CAst
 open Names
 open Nameops
-open Constr
 open Namegen
+open Constr
 open Libnames
 open Globnames
 open Impargs
@@ -394,7 +394,7 @@ let intern_generalized_binder ?(global_level=false) intern_type ntnvars
     env fvs in
   let bl = List.map
     CAst.(map (fun id ->
-      (Name id, b, DAst.make ?loc @@ GHole (Evar_kinds.BinderType (Name id), Misctypes.IntroAnonymous, None))))
+      (Name id, b, DAst.make ?loc @@ GHole (Evar_kinds.BinderType (Name id), IntroAnonymous, None))))
     fvs
   in
   let na = match na with
@@ -431,7 +431,7 @@ let glob_local_binder_of_extended = DAst.with_loc_val (fun ?loc -> function
   | GLocalAssum (na,bk,t) -> (na,bk,None,t)
   | GLocalDef (na,bk,c,Some t) -> (na,bk,Some c,t)
   | GLocalDef (na,bk,c,None) ->
-      let t = DAst.make ?loc @@ GHole(Evar_kinds.BinderType na,Misctypes.IntroAnonymous,None) in
+      let t = DAst.make ?loc @@ GHole(Evar_kinds.BinderType na,IntroAnonymous,None) in
       (na,bk,Some c,t)
   | GLocalPattern (_,_,_,_) ->
       Loc.raise ?loc (Stream.Error "pattern with quote not allowed here")
@@ -472,7 +472,7 @@ let intern_local_binder_aux ?(global_level=false) intern ntnvars (env,bl) = func
       let tyc =
         match ty with
         | Some ty -> ty
-        | None -> CAst.make ?loc @@ CHole(None,Misctypes.IntroAnonymous,None)
+        | None -> CAst.make ?loc @@ CHole(None,IntroAnonymous,None)
       in
       let env, ((disjpat,il),id),na = intern_cases_pattern_as_binder ?loc ntnvars env p in
       let bk = Default Explicit in
@@ -502,11 +502,11 @@ let intern_generalization intern env ntnvars loc bk ak c =
 	if pi then
           (fun {loc=loc';v=id} acc ->
             DAst.make ?loc:(Loc.merge_opt loc' loc) @@
-	    GProd (Name id, bk, DAst.make ?loc:loc' @@ GHole (Evar_kinds.BinderType (Name id), Misctypes.IntroAnonymous, None), acc))
+            GProd (Name id, bk, DAst.make ?loc:loc' @@ GHole (Evar_kinds.BinderType (Name id), IntroAnonymous, None), acc))
 	else
           (fun {loc=loc';v=id} acc ->
             DAst.make ?loc:(Loc.merge_opt loc' loc) @@
-	    GLambda (Name id, bk, DAst.make ?loc:loc' @@ GHole (Evar_kinds.BinderType (Name id), Misctypes.IntroAnonymous, None), acc))
+            GLambda (Name id, bk, DAst.make ?loc:loc' @@ GHole (Evar_kinds.BinderType (Name id), IntroAnonymous, None), acc))
     in
       List.fold_right (fun ({loc;v=id} as lid) (env, acc) ->
         let env' = push_name_env ntnvars (Variable,[],[],[]) env CAst.(make @@ Name id) in
@@ -564,7 +564,7 @@ let term_of_name = function
   | Name id -> DAst.make (GVar id)
   | Anonymous ->
        let st = Evar_kinds.Define (not (Program.get_proofs_transparency ())) in
-       DAst.make (GHole (Evar_kinds.QuestionMark (st,Anonymous), Misctypes.IntroAnonymous, None))
+       DAst.make (GHole (Evar_kinds.QuestionMark (st,Anonymous), IntroAnonymous, None))
 
 let traverse_binder intern_pat ntnvars (terms,_,binders,_ as subst) avoid (renaming,env) = function
  | Anonymous -> (renaming,env), None, Anonymous
@@ -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 *)
@@ -626,7 +626,7 @@ let terms_of_binders bl =
     | PatVar (Anonymous) -> error_cannot_coerce_wildcard_term ?loc ()
     | PatCstr (c,l,_) ->
        let r = make ?loc @@ Qualid (qualid_of_path (path_of_global (ConstructRef c))) in
-       let hole = CAst.make ?loc @@ CHole (None,Misctypes.IntroAnonymous,None) in
+       let hole = CAst.make ?loc @@ CHole (None,IntroAnonymous,None) in
        let params = List.make (Inductiveops.inductive_nparams (fst c)) hole in
        CAppExpl ((None,r,None),params @ List.map term_of_pat l)) pt in
   let rec extract_variables l = match l with
@@ -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;
 }
 
@@ -1725,15 +1725,15 @@ let get_implicit_name n imps =
 let set_hole_implicit i b c =
   let loc = c.CAst.loc in
   match DAst.get c with
-  | GRef (r, _) -> Loc.tag ?loc (Evar_kinds.ImplicitArg (r,i,b),Misctypes.IntroAnonymous,None)
+  | GRef (r, _) -> Loc.tag ?loc (Evar_kinds.ImplicitArg (r,i,b),IntroAnonymous,None)
   | GApp (r, _) ->
     let loc = r.CAst.loc in
     begin match DAst.get r with
     | GRef (r, _) ->
-      Loc.tag ?loc (Evar_kinds.ImplicitArg (r,i,b),Misctypes.IntroAnonymous,None)
+      Loc.tag ?loc (Evar_kinds.ImplicitArg (r,i,b),IntroAnonymous,None)
     | _ -> anomaly (Pp.str "Only refs have implicits.")
     end
-  | GVar id -> Loc.tag ?loc (Evar_kinds.ImplicitArg (VarRef id,i,b),Misctypes.IntroAnonymous,None)
+  | GVar id -> Loc.tag ?loc (Evar_kinds.ImplicitArg (VarRef id,i,b),IntroAnonymous,None)
   | _ -> anomaly (Pp.str "Only refs have implicits.")
 
 let exists_implicit_name id =
@@ -1919,13 +1919,13 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
        let fields =
 	 sort_fields ~complete:true loc fs
 	             (fun _idx -> CAst.make ?loc @@ CHole (Some (Evar_kinds.QuestionMark (st,Anonymous)),
-                                                           Misctypes.IntroAnonymous, None))
+                                                           IntroAnonymous, None))
        in
        begin
 	  match fields with
 	    | None -> user_err ?loc ~hdr:"intern" (str"No constructor inference.")
 	    | Some (n, constrname, args) ->
-		let pars = List.make n (CAst.make ?loc @@ CHole (None, Misctypes.IntroAnonymous, None)) in
+                let pars = List.make n (CAst.make ?loc @@ CHole (None, IntroAnonymous, None)) in
                 let app = CAst.make ?loc @@ CAppExpl ((None, constrname,None), List.rev_append pars args) in
 	  intern env app
 	end
@@ -1965,12 +1965,12 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
              let main_sub_eqn = CAst.make @@
                ([],thepats, (* "|p1,..,pn" *)
 		Option.cata (intern_type env')
-                  (DAst.make ?loc @@ GHole(Evar_kinds.CasesType false,Misctypes.IntroAnonymous,None))
+                  (DAst.make ?loc @@ GHole(Evar_kinds.CasesType false,IntroAnonymous,None))
                   rtnpo) (* "=> P" if there were a return predicate P, and "=> _" otherwise *) in
              let catch_all_sub_eqn =
                if List.for_all (irrefutable globalenv) thepats then [] else
                   [CAst.make @@ ([],List.make (List.length thepats) (DAst.make @@ PatVar Anonymous), (* "|_,..,_" *)
-                   DAst.make @@ GHole(Evar_kinds.ImpossibleCase,Misctypes.IntroAnonymous,None))]   (* "=> _" *) in
+                   DAst.make @@ GHole(Evar_kinds.ImpossibleCase,IntroAnonymous,None))]   (* "=> _" *) in
              Some (DAst.make @@ GCases(RegularStyle,sub_rtn,sub_tms,main_sub_eqn::catch_all_sub_eqn))
 	in
         let eqns' = List.map (intern_eqn (List.length tms) env) eqns in
@@ -2001,7 +2001,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
         | None ->
            let st = Evar_kinds.Define (not (Program.get_proofs_transparency ())) in
            (match naming with
-           | Misctypes.IntroIdentifier id -> Evar_kinds.NamedHole id
+           | IntroIdentifier id -> Evar_kinds.NamedHole id
            | _ -> Evar_kinds.QuestionMark (st,Anonymous))
         | Some k -> k
         in
@@ -2046,7 +2046,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
 	GSort s
     | CCast (c1, c2) ->
 	DAst.make ?loc @@
-        GCast (intern env c1, Miscops.map_cast_type (intern_type env) c2)
+        GCast (intern env c1, map_cast_type (intern_type env) c2)
     | CProj (pr, c) ->
       match intern_reference pr with
       | ConstRef p ->
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/genintern.ml b/interp/genintern.ml
index 161201c44..d9a0db040 100644
--- a/interp/genintern.ml
+++ b/interp/genintern.ml
@@ -26,9 +26,15 @@ let empty_glob_sign env = {
   extra = Store.empty;
 }
 
+(** In globalize tactics, we need to keep the initial [constr_expr] to recompute
+   in the environment by the effective calls to Intro, Inversion, etc
+   The [constr_expr] field is [None] in TacDef though *)
+type glob_constr_and_expr = Glob_term.glob_constr * Constrexpr.constr_expr option
+type glob_constr_pattern_and_expr = Id.Set.t * glob_constr_and_expr * Pattern.constr_pattern
+
 type ('raw, 'glb) intern_fun = glob_sign -> 'raw -> glob_sign * 'glb
 type 'glb subst_fun = substitution -> 'glb -> 'glb
-type 'glb ntn_subst_fun = Tactypes.glob_constr_and_expr Id.Map.t -> 'glb -> 'glb
+type 'glb ntn_subst_fun = glob_constr_and_expr Id.Map.t -> 'glb -> 'glb
 
 module InternObj =
 struct
diff --git a/interp/genintern.mli b/interp/genintern.mli
index d818713fc..f4f064bca 100644
--- a/interp/genintern.mli
+++ b/interp/genintern.mli
@@ -22,6 +22,12 @@ type glob_sign = {
 
 val empty_glob_sign : Environ.env -> glob_sign
 
+(** In globalize tactics, we need to keep the initial [constr_expr] to recompute
+   in the environment by the effective calls to Intro, Inversion, etc
+   The [constr_expr] field is [None] in TacDef though *)
+type glob_constr_and_expr = Glob_term.glob_constr * Constrexpr.constr_expr option
+type glob_constr_pattern_and_expr = Id.Set.t * glob_constr_and_expr * Pattern.constr_pattern
+
 (** {5 Internalization functions} *)
 
 type ('raw, 'glb) intern_fun = glob_sign -> 'raw -> glob_sign * 'glb
@@ -42,7 +48,7 @@ val generic_substitute : glob_generic_argument subst_fun
 
 (** {5 Notation functions} *)
 
-type 'glb ntn_subst_fun = Tactypes.glob_constr_and_expr Id.Map.t -> 'glb -> 'glb
+type 'glb ntn_subst_fun = glob_constr_and_expr Id.Map.t -> 'glb -> 'glb
 
 val substitute_notation : ('raw, 'glb, 'top) genarg_type -> 'glb ntn_subst_fun
 
diff --git a/interp/genredexpr.ml b/interp/genredexpr.ml
index 80697461a..42c1fe429 100644
--- a/interp/genredexpr.ml
+++ b/interp/genredexpr.ml
@@ -52,12 +52,11 @@ 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
 open Constrexpr
-open Misctypes
 
 type r_trm = constr_expr
 type r_pat = constr_pattern_expr
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/modintern.ml b/interp/modintern.ml
index fefd2ab6f..33c07d551 100644
--- a/interp/modintern.ml
+++ b/interp/modintern.ml
@@ -12,7 +12,7 @@ open Declarations
 open Libnames
 open Constrexpr
 open Constrintern
-open Misctypes
+open Declaremods
 
 type module_internalization_error =
   | NotAModuleNorModtype of string
@@ -23,7 +23,7 @@ exception ModuleInternalizationError of module_internalization_error
 
 let error_not_a_module_loc kind loc qid =
   let s = string_of_qualid qid in
-  let e = match kind with
+  let e = let open Declaremods in match kind with
     | Module -> Modops.ModuleTypingError (Modops.NotAModule s)
     | ModType -> Modops.ModuleTypingError (Modops.NotAModuleType s)
     | ModAny -> ModuleInternalizationError (NotAModuleNorModtype s)
@@ -46,6 +46,7 @@ let error_application_to_module_type loc =
     it is equal to the input kind when this one isn't ModAny. *)
 
 let lookup_module_or_modtype kind {CAst.loc;v=qid} =
+  let open Declaremods in
   try
     if kind == ModType then raise Not_found;
     let mp = Nametab.locate_module qid in
diff --git a/interp/modintern.mli b/interp/modintern.mli
index ef37aead8..529c438c1 100644
--- a/interp/modintern.mli
+++ b/interp/modintern.mli
@@ -11,7 +11,6 @@
 open Environ
 open Entries
 open Constrexpr
-open Misctypes
 
 (** Module internalization errors *)
 
@@ -30,4 +29,4 @@ exception ModuleInternalizationError of module_internalization_error
    isn't ModAny. *)
 
 val interp_module_ast :
-  env -> module_kind -> module_ast -> module_struct_entry * module_kind * Univ.ContextSet.t
+  env -> Declaremods.module_kind -> module_ast -> module_struct_entry * Declaremods.module_kind * Univ.ContextSet.t
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index f208b23fb..ab0bf9c6f 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -16,7 +16,7 @@ open Nameops
 open Constr
 open Globnames
 open Decl_kinds
-open Misctypes
+open Namegen
 open Glob_term
 open Glob_ops
 open Mod_subst
@@ -86,7 +86,7 @@ let rec eq_notation_constr (vars1,vars2 as vars) t1 t2 = match t1, t2 with
   Array.equal (eq_notation_constr vars) us1 us2 &&
   Array.equal (eq_notation_constr vars) rs1 rs2
 | NSort s1, NSort s2 ->
-  Miscops.glob_sort_eq s1 s2
+  glob_sort_eq s1 s2
 | NCast (t1, c1), NCast (t2, c2) ->
   (eq_notation_constr vars) t1 t2 && cast_type_eq (eq_notation_constr vars) c1 c2
 | NProj (p1, c1), NProj (p2, c2) ->
@@ -158,7 +158,7 @@ let protect g e na =
 let apply_cases_pattern ?loc ((ids,disjpat),id) c =
   let tm = DAst.make ?loc (GVar id) in
   let eqns = List.map (fun pat -> (CAst.make ?loc (ids,[pat],c))) disjpat in
-  DAst.make ?loc @@ GCases (LetPatternStyle, None, [tm,(Anonymous,None)], eqns)
+  DAst.make ?loc @@ GCases (Constr.LetPatternStyle, None, [tm,(Anonymous,None)], eqns)
 
 let glob_constr_of_notation_constr_with_binders ?loc g f e nc =
   let lt x = DAst.make ?loc x in lt @@ match nc with
@@ -216,7 +216,7 @@ let glob_constr_of_notation_constr_with_binders ?loc g f e nc =
 	  (e,(na,Explicit,Option.map (f e) oc,f e b)))) e dll in
       let e',idl = Array.fold_left_map (to_id (protect g)) e idl in
       GRec (fk,idl,dll,Array.map (f e) tl,Array.map (f e') bl)
-  | NCast (c,k) -> GCast (f e c,Miscops.map_cast_type (f e) k)
+  | NCast (c,k) -> GCast (f e c,map_cast_type (f e) k)
   | NSort x -> GSort x
   | NHole (x, naming, arg)  -> GHole (x, naming, arg)
   | NRef x -> GRef (x,None)
@@ -434,7 +434,7 @@ let notation_constr_and_vars_of_glob_constr recvars a =
 	   user_err Pp.(str "Binders marked as implicit not allowed in notations.");
 	 add_name found na; (na,Option.map aux oc,aux b))) dll in
       NRec (fk,idl,dll,Array.map aux tl,Array.map aux bl)
-  | GCast (c,k) -> NCast (aux c,Miscops.map_cast_type aux k)
+  | GCast (c,k) -> NCast (aux c,map_cast_type aux k)
   | GSort s -> NSort s
   | GHole (w,naming,arg) ->
      if arg != None then has_ltac := true;
@@ -637,7 +637,7 @@ let rec subst_notation_constr subst bound raw =
 
   | NCast (r1,k) ->
       let r1' = subst_notation_constr subst bound r1 in
-      let k' = Miscops.smartmap_cast_type (subst_notation_constr subst bound) k in
+      let k' = smartmap_cast_type (subst_notation_constr subst bound) k in
       if r1' == r1 && k' == k then raw else NCast(r1',k')
 
   | NProj (p, c) ->
@@ -666,11 +666,11 @@ let abstract_return_type_context pi mklam tml rtno =
 let abstract_return_type_context_glob_constr tml rtn =
   abstract_return_type_context (fun {CAst.v=(_,nal)} -> nal)
     (fun na c -> DAst.make @@
-      GLambda(na,Explicit,DAst.make @@ GHole(Evar_kinds.InternalHole,Misctypes.IntroAnonymous,None),c)) tml rtn
+      GLambda(na,Explicit,DAst.make @@ GHole(Evar_kinds.InternalHole,IntroAnonymous,None),c)) tml rtn
 
 let abstract_return_type_context_notation_constr tml rtn =
   abstract_return_type_context snd
-    (fun na c -> NLambda(na,NHole (Evar_kinds.InternalHole, Misctypes.IntroAnonymous, None),c)) tml rtn
+    (fun na c -> NLambda(na,NHole (Evar_kinds.InternalHole, IntroAnonymous, None),c)) tml rtn
 
 let is_term_meta id metas =
   try match Id.List.assoc id metas with _,(NtnTypeConstr | NtnTypeConstrList) -> true | _ -> false
@@ -1194,7 +1194,7 @@ let rec match_ inner u alp metas sigma a1 a2 =
   | GCast(t1, c1), NCast(t2, c2) ->
     match_cast (match_in u alp metas) (match_in u alp metas sigma t1 t2) c1 c2
   | GSort (GType _), NSort (GType _) when not u -> sigma
-  | GSort s1, NSort s2 when Miscops.glob_sort_eq s1 s2 -> sigma
+  | GSort s1, NSort s2 when glob_sort_eq s1 s2 -> sigma
   | GPatVar _, NHole _ -> (*Don't hide Metas, they bind in ltac*) raise No_match
   | a, NHole _ -> sigma
 
@@ -1208,7 +1208,7 @@ let rec match_ inner u alp metas sigma a1 a2 =
       let avoid =
         Id.Set.union (free_glob_vars a1) (* as in Namegen: *) (glob_visible_short_qualid a1) in
       let id' = Namegen.next_ident_away id avoid in
-      let t1 = DAst.make @@ GHole(Evar_kinds.BinderType (Name id'),Misctypes.IntroAnonymous,None) in
+      let t1 = DAst.make @@ GHole(Evar_kinds.BinderType (Name id'),IntroAnonymous,None) in
       let sigma = match t2 with
       | NHole _ -> sigma
       | NVar id2 -> bind_term_env alp sigma id2 t1
@@ -1241,7 +1241,7 @@ and match_extended_binders ?loc isprod u alp metas na1 na2 bk t sigma b1 b2 =
   let store, get = set_temporary_memory () in
   match na1, DAst.get b1, na2 with
   (* Matching individual binders as part of a recursive pattern *)
-  | Name p, GCases (LetPatternStyle,None,[(e,_)],(_::_ as eqns)), Name id
+  | Name p, GCases (Constr.LetPatternStyle,None,[(e,_)],(_::_ as eqns)), Name id
        when is_gvar p e && is_bindinglist_meta id metas && List.length (store (Detyping.factorize_eqns eqns)) = 1 ->
     (match get () with
      | [{CAst.v=(ids,disj_of_patl,b1)}] ->
diff --git a/interp/notation_term.ml b/interp/notation_term.ml
index 52a6354a0..6d9effcef 100644
--- a/interp/notation_term.ml
+++ b/interp/notation_term.ml
@@ -9,7 +9,6 @@
 (************************************************************************)
 
 open Names
-open Misctypes
 open Glob_term
 
 (** [notation_constr] *)
@@ -25,7 +24,7 @@ type notation_constr =
   | NRef of GlobRef.t
   | NVar of Id.t
   | NApp of notation_constr * notation_constr list
-  | NHole of Evar_kinds.t * Misctypes.intro_pattern_naming_expr * Genarg.glob_generic_argument option
+  | NHole of Evar_kinds.t * Namegen.intro_pattern_naming_expr * Genarg.glob_generic_argument option
   | NList of Id.t * Id.t * notation_constr * notation_constr * (* associativity: *) bool
   (** Part only in [glob_constr] *)
   | NLambda of Name.t * notation_constr * notation_constr
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/interp/smartlocate.ml b/interp/smartlocate.ml
index 1f4a93a6f..e1fbdba87 100644
--- a/interp/smartlocate.ml
+++ b/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) ->
diff --git a/interp/smartlocate.mli b/interp/smartlocate.mli
index 45037b8b3..6b574d7b5 100644
--- a/interp/smartlocate.mli
+++ b/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
diff --git a/interp/stdarg.ml b/interp/stdarg.ml
index e5ed58be6..7b01b6dc1 100644
--- a/interp/stdarg.ml
+++ b/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
@@ -34,9 +36,6 @@ let wit_pre_ident : string uniform_genarg_type =
 let wit_int_or_var =
   make0 ~dyn:(val_tag (topwit wit_int)) "int_or_var"
 
-let wit_intro_pattern =
-  make0 "intropattern"
-
 let wit_ident =
   make0 "ident"
 
@@ -45,8 +44,6 @@ let wit_var =
 
 let wit_ref = make0 "ref"
 
-let wit_quant_hyp = make0 "quant_hyp"
-
 let wit_sort_family = make0 "sort_family"
 
 let wit_constr =
@@ -56,12 +53,6 @@ let wit_uconstr = make0 "uconstr"
 
 let wit_open_constr = make0 ~dyn:(val_tag (topwit wit_constr)) "open_constr"
 
-let wit_constr_with_bindings = make0 "constr_with_bindings"
-
-let wit_open_constr_with_bindings = make0 "open_constr_with_bindings"
-
-let wit_bindings = make0 "bindings"
-
 let wit_red_expr = make0 "redexpr"
 
 let wit_clause_dft_concl  =
@@ -74,6 +65,4 @@ let wit_preident = wit_pre_ident
 let wit_reference = wit_ref
 let wit_global = wit_ref
 let wit_clause = wit_clause_dft_concl
-let wit_quantified_hypothesis = wit_quant_hyp
-let wit_intropattern = wit_intro_pattern
 let wit_redexpr = wit_red_expr
diff --git a/interp/stdarg.mli b/interp/stdarg.mli
index dc9c370a1..4792cda08 100644
--- a/interp/stdarg.mli
+++ b/interp/stdarg.mli
@@ -17,9 +17,11 @@ open Libnames
 open Genredexpr
 open Pattern
 open Constrexpr
-open Misctypes
-open Tactypes
 open Genarg
+open Genintern
+open Locus
+
+type 'a and_short_name = 'a * lident option
 
 val wit_unit : unit uniform_genarg_type
 
@@ -35,16 +37,12 @@ val wit_pre_ident : string uniform_genarg_type
 
 val wit_int_or_var : (int or_var, int or_var, int) genarg_type
 
-val wit_intro_pattern : (constr_expr intro_pattern_expr CAst.t, glob_constr_and_expr intro_pattern_expr CAst.t, intro_pattern) genarg_type
-
 val wit_ident : Id.t uniform_genarg_type
 
 val wit_var : (lident, lident, Id.t) genarg_type
 
 val wit_ref : (reference, GlobRef.t located or_var, GlobRef.t) genarg_type
 
-val wit_quant_hyp : quantified_hypothesis uniform_genarg_type
-
 val wit_sort_family : (Sorts.family, unit, unit) genarg_type
 
 val wit_constr : (constr_expr, glob_constr_and_expr, constr) genarg_type
@@ -54,21 +52,6 @@ val wit_uconstr : (constr_expr , glob_constr_and_expr, Ltac_pretype.closed_glob_
 val wit_open_constr :
   (constr_expr, glob_constr_and_expr, constr) genarg_type
 
-val wit_constr_with_bindings :
-  (constr_expr with_bindings,
-  glob_constr_and_expr with_bindings,
-  constr with_bindings delayed_open) genarg_type
-
-val wit_open_constr_with_bindings :
-  (constr_expr with_bindings,
-  glob_constr_and_expr with_bindings,
-  constr with_bindings delayed_open) genarg_type
-
-val wit_bindings :
-  (constr_expr bindings,
-  glob_constr_and_expr bindings,
-  constr bindings delayed_open) genarg_type
-
 val wit_red_expr :
   ((constr_expr,reference or_by_notation,constr_expr) red_expr_gen,
   (glob_constr_and_expr,evaluable_global_reference and_short_name or_var,glob_constr_pattern_and_expr) red_expr_gen,
@@ -83,8 +66,6 @@ val wit_preident : string uniform_genarg_type
 val wit_reference : (reference, GlobRef.t located or_var, GlobRef.t) genarg_type
 val wit_global : (reference, GlobRef.t located or_var, GlobRef.t) genarg_type
 val wit_clause :  (lident Locus.clause_expr, lident Locus.clause_expr, Names.Id.t Locus.clause_expr) genarg_type
-val wit_quantified_hypothesis : quantified_hypothesis uniform_genarg_type
-val wit_intropattern : (constr_expr intro_pattern_expr CAst.t, glob_constr_and_expr intro_pattern_expr CAst.t, intro_pattern) genarg_type
 val wit_redexpr :
   ((constr_expr,reference or_by_notation,constr_expr) red_expr_gen,
   (glob_constr_and_expr,evaluable_global_reference and_short_name or_var,glob_constr_pattern_and_expr) red_expr_gen,
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 1d5df49cf..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} *)
 
@@ -36,6 +35,8 @@ type inline =
   | DefaultInline
   | InlineAt of int
 
+type module_kind = Module | ModType | ModAny
+
 let default_inline () = Some (Flags.get_inline_level ())
 
 let inl2intopt = function
@@ -994,8 +995,8 @@ let iter_all_segments f =
 (** {6 Some types used to shorten declaremods.mli} *)
 
 type 'modast module_interpretor =
-  Environ.env -> Misctypes.module_kind -> 'modast ->
-    Entries.module_struct_entry * Misctypes.module_kind * Univ.ContextSet.t
+  Environ.env -> module_kind -> 'modast ->
+    Entries.module_struct_entry * module_kind * Univ.ContextSet.t
 
 type 'modast module_params =
   (lident list * ('modast * inline)) list
diff --git a/library/declaremods.mli b/library/declaremods.mli
index 4aee7feae..b42a59bfb 100644
--- a/library/declaremods.mli
+++ b/library/declaremods.mli
@@ -27,12 +27,16 @@ type inline =
   | DefaultInline
   | InlineAt of int
 
+(** Kinds of modules *)
+
+type module_kind = Module | ModType | ModAny
+
 type 'modast module_interpretor =
-  Environ.env -> Misctypes.module_kind -> 'modast ->
-    Entries.module_struct_entry * Misctypes.module_kind * Univ.ContextSet.t
+  Environ.env -> module_kind -> 'modast ->
+    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/library.mllib b/library/library.mllib
index 1c0368847..2ac4266fc 100644
--- a/library/library.mllib
+++ b/library/library.mllib
@@ -6,7 +6,6 @@ Nametab
 Global
 Decl_kinds
 Lib
-Misctypes
 Declaremods
 Loadpath
 Library
diff --git a/library/misctypes.ml b/library/misctypes.ml
deleted file mode 100644
index cfae07484..000000000
--- a/library/misctypes.ml
+++ /dev/null
@@ -1,114 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
-(* <O___,, *       (see CREDITS file for the list of authors)           *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-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 =
-  | IntroForthcoming of bool
-  | IntroNaming of intro_pattern_naming_expr
-  | IntroAction of 'constr intro_pattern_action_expr
-and intro_pattern_naming_expr =
-  | IntroIdentifier of Id.t
-  | IntroFresh of Id.t
-  | IntroAnonymous
-and 'constr intro_pattern_action_expr =
-  | IntroWildcard
-  | IntroOrAndPattern of 'constr or_and_intro_pattern_expr
-  | IntroInjection of ('constr intro_pattern_expr) CAst.t list
-  | IntroApplyOn of 'constr CAst.t * 'constr intro_pattern_expr CAst.t
-  | IntroRewrite of bool
-and 'constr or_and_intro_pattern_expr =
-  | IntroOrPattern of ('constr intro_pattern_expr) CAst.t list list
-  | IntroAndPattern of ('constr intro_pattern_expr) CAst.t list
-
-(** Move destination for hypothesis *)
-
-type 'id move_location =
-  | MoveAfter of 'id
-  | MoveBefore of 'id
-  | MoveFirst
-  | MoveLast (** can be seen as "no move" when doing intro *)
-
-(** A synonym of [Evar.t], also defined in Term *)
-
-type existential_key = Evar.t
-
-(** Casts *)
-
-type 'a cast_type =
-  | CastConv of 'a
-  | CastVM of 'a
-  | CastCoerce (** Cast to a base type (eg, an underlying inductive type) *)
-  | CastNative of 'a
-
-(** Bindings *)
-
-type quantified_hypothesis = AnonHyp of int | NamedHyp of Id.t
-
-type 'a explicit_bindings = (quantified_hypothesis * 'a) CAst.t list
-
-type 'a bindings =
-  | ImplicitBindings of 'a list
-  | ExplicitBindings of 'a explicit_bindings
-  | NoBindings
-
-type 'a with_bindings = 'a * 'a bindings
-
-
-(** Some utility types for parsing *)
-
-type 'a or_var =
-  | ArgArg of 'a
-  | ArgVar of lident
-
-type 'a and_short_name = 'a * lident option
-
-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. *)
-
-
-(** Kinds of modules *)
-
-type module_kind = Module | ModType | ModAny
-
-(** Various flags *)
-
-type direction_flag = bool (* true = Left-to-right    false = right-to-right *)
-type evars_flag = bool     (* true = pose evars       false = fail on evars *)
-type rec_flag = bool       (* true = recursive        false = not recursive *)
-type advanced_flag = bool  (* true = advanced         false = basic *)
-type letin_flag = bool     (* true = use local def    false = use Leibniz *)
-type clear_flag = bool option (* true = clear hyp, false = keep hyp, None = use default *)
-
-type multi =
-  | Precisely of int
-  | UpTo of int
-  | RepeatStar
-  | RepeatPlus
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index f8af79cd7..94149a085 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -16,7 +16,7 @@ open Constrexpr
 open Constrexpr_ops
 open Util
 open Tok
-open Misctypes
+open Namegen
 open Decl_kinds
 
 open Pcoq
diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4
index b25ea766a..08bcd0f8c 100644
--- a/parsing/g_prim.ml4
+++ b/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 ] ]
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 00ca53884..9a45bc973 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -13,7 +13,6 @@ open Extend
 open Genarg
 open Constrexpr
 open Libnames
-open Misctypes
 
 (** The parser of Coq *)
 
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 361981c5b..04ff11fc4 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -443,7 +443,7 @@ let cc_tactic depth additionnal_terms =
             let open Glob_term in
             let env = Proofview.Goal.env gl in
             let terms_to_complete = List.map (build_term_to_complete uf) (epsilons uf) in
-            let hole = DAst.make @@ GHole (Evar_kinds.InternalHole, Misctypes.IntroAnonymous, None) in
+            let hole = DAst.make @@ GHole (Evar_kinds.InternalHole, Namegen.IntroAnonymous, None) in
             let pr_missing (c, missing) =
               let c = Detyping.detype Detyping.Now ~lax:true false Id.Set.empty env sigma c in
               let holes = List.init missing (fun _ -> hole) in
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index bebd27e11..1e0589fac 100644
--- a/plugins/extraction/extract_env.ml
+++ b/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],[] ->
diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index 22a3e1f67..85f493956 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -22,7 +22,6 @@ open Reductionops
 open Formula
 open Sequent
 open Names
-open Misctypes
 open Context.Rel.Declaration
 
 let compare_instance inst1 inst2=
@@ -184,12 +183,12 @@ let right_instance_tac inst continue seq=
 	   [introf;
             Proofview.Goal.enter begin fun gl ->
               let id0 = List.nth (pf_ids_of_hyps gl) 0 in
-              split (ImplicitBindings [mkVar id0])
+              split (Tactypes.ImplicitBindings [mkVar id0])
             end;
 	    tclSOLVE [wrap 0 true continue (deepen seq)]];
 	 tclTRY assumption]
     | Real ((0,t),_) ->
-	(tclTHEN (split (ImplicitBindings [t]))
+        (tclTHEN (split (Tactypes.ImplicitBindings [t]))
 	   (tclSOLVE [wrap 0 true continue (deepen seq)]))
     | Real ((m,t),_) ->
 	tclFAIL 0 (Pp.str "not implemented ... yet")
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index 0a2741ad1..9899b7b21 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -15,7 +15,8 @@ open Indfun_common
 open Indfun
 open Genarg
 open Stdarg
-open Misctypes
+open Tacarg
+open Tactypes
 open Pcoq
 open Pcoq.Prim
 open Pcoq.Constr
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 3ba3bafa4..6b9b10312 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -10,7 +10,6 @@ open Indfun_common
 open CErrors
 open Util
 open Glob_termops
-open Misctypes
 
 module RelDecl = Context.Rel.Declaration
 module NamedDecl = Context.Named.Declaration
diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml
index bb1587507..954fc3bab 100644
--- a/plugins/funind/glob_termops.ml
+++ b/plugins/funind/glob_termops.ml
@@ -5,7 +5,6 @@ open CErrors
 open Util
 open Names
 open Decl_kinds
-open Misctypes
 
 (*
    Some basic functions to rebuild glob_constr
@@ -18,7 +17,7 @@ let mkGLambda(n,t,b)    = DAst.make @@ GLambda(n,Explicit,t,b)
 let mkGProd(n,t,b)      = DAst.make @@ GProd(n,Explicit,t,b)
 let mkGLetIn(n,b,t,c)   = DAst.make @@ GLetIn(n,b,t,c)
 let mkGCases(rto,l,brl) = DAst.make @@ GCases(RegularStyle,rto,l,brl)
-let mkGHole ()          = DAst.make @@ GHole(Evar_kinds.BinderType Anonymous,Misctypes.IntroAnonymous,None)
+let mkGHole ()          = DAst.make @@ GHole(Evar_kinds.BinderType Anonymous,Namegen.IntroAnonymous,None)
 
 (*
   Some basic functions to decompose glob_constrs
@@ -109,7 +108,7 @@ let change_vars =
       | GHole _ as x -> x
       | GCast(b,c) ->
 	  GCast(change_vars mapping b,
-		Miscops.map_cast_type (change_vars mapping) c)
+                Glob_ops.map_cast_type (change_vars mapping) c)
       | GProj(p,c) -> GProj(p, change_vars mapping c)
       ) rt
   and change_vars_br mapping ({CAst.loc;v=(idl,patl,res)} as br) =
@@ -290,7 +289,7 @@ let rec alpha_rt excluded rt =
     | GHole _ as rt -> rt
     | GCast (b,c) ->
 	GCast(alpha_rt excluded b,
-	      Miscops.map_cast_type (alpha_rt excluded) c)
+              Glob_ops.map_cast_type (alpha_rt excluded) c)
     | GApp(f,args) ->
 	GApp(alpha_rt excluded f,
 	     List.map (alpha_rt excluded) args
@@ -440,7 +439,7 @@ let replace_var_by_term x_id term =
       | GHole _ as rt -> rt
       | GCast(b,c) ->
 	  GCast(replace_var_by_pattern b,
-		Miscops.map_cast_type replace_var_by_pattern c)
+                Glob_ops.map_cast_type replace_var_by_pattern c)
       | GProj(p,c) ->
         GProj(p,replace_var_by_pattern c)
     ) x
@@ -542,7 +541,7 @@ let expand_as =
       | GRec _ ->  user_err Pp.(str "Not handled GRec")
       | GCast(b,c) ->
 	  GCast(expand_as map b,
-		Miscops.map_cast_type (expand_as map) c)
+                Glob_ops.map_cast_type (expand_as map) c)
       | GCases(sty,po,el,brl) ->
 	  GCases(sty, Option.map (expand_as map) po, List.map (fun (rt,t) -> expand_as map rt,t) el,
 		List.map (expand_as_br map) brl)
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index efbd029e4..cd640eebd 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -10,7 +10,7 @@ open Libnames
 open Globnames
 open Glob_term
 open Declarations
-open Misctypes
+open Tactypes
 open Decl_kinds
 
 module RelDecl = Context.Rel.Declaration
@@ -782,7 +782,7 @@ let rec add_args id new_args = CAst.map (function
   | CSort _ as b -> b
   | CCast(b1,b2)  ->
       CCast(add_args id new_args b1,
-	    Miscops.map_cast_type (add_args id new_args) b2)
+            Glob_ops.map_cast_type (add_args id new_args) b2)
   | CRecord pars ->
       CRecord (List.map (fun (e,o) -> e, add_args id new_args o) pars)
   | CNotation _ -> anomaly ~label:"add_args " (Pp.str "CNotation.")
diff --git a/plugins/funind/indfun.mli b/plugins/funind/indfun.mli
index 24304e361..f209fb19f 100644
--- a/plugins/funind/indfun.mli
+++ b/plugins/funind/indfun.mli
@@ -1,5 +1,5 @@
 open Names
-open Misctypes
+open Tactypes
 
 val warn_cannot_define_graph : ?loc:Loc.t -> Pp.t * Pp.t -> unit
 
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index cc92a73f0..439274240 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -23,7 +23,7 @@ open Tacticals
 open Tactics
 open Indfun_common
 open Tacmach
-open Misctypes
+open Tactypes
 open Termops
 open Context.Rel.Declaration
 
@@ -239,7 +239,7 @@ let prove_fun_correct evd funs_constr graphs_constr schemes lemmas_types_infos i
       List.map
 	(fun decl ->
 	   List.map
-             (fun id -> CAst.make @@ IntroNaming (IntroIdentifier id))
+             (fun id -> CAst.make @@ IntroNaming (Namegen.IntroIdentifier id))
 	     (generate_fresh_id (Id.of_string "y") ids (List.length (fst (decompose_prod_assum evd (RelDecl.get_type decl)))))
 	)
 	branches
@@ -257,7 +257,7 @@ let prove_fun_correct evd funs_constr graphs_constr schemes lemmas_types_infos i
       	List.fold_right
           (fun {CAst.v=pat} acc ->
       	     match pat with
-	       | IntroNaming (IntroIdentifier id) -> id::acc
+               | IntroNaming (Namegen.IntroIdentifier id) -> id::acc
       	       | _ -> anomaly (Pp.str "Not an identifier.")
       	  )
       	  (List.nth intro_pats (pred i))
diff --git a/plugins/funind/invfun.mli b/plugins/funind/invfun.mli
index 9151fd0e2..3ddc60920 100644
--- a/plugins/funind/invfun.mli
+++ b/plugins/funind/invfun.mli
@@ -9,7 +9,7 @@
 (************************************************************************)
 
 val invfun :
-  Misctypes.quantified_hypothesis ->
+  Tactypes.quantified_hypothesis ->
   Names.GlobRef.t option ->
   Evar.t Evd.sigma -> Evar.t list Evd.sigma
 val derive_correctness :
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 72bb8253d..aa49148fc 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -37,7 +37,7 @@ open Glob_term
 open Pretyping
 open Termops
 open Constrintern
-open Misctypes
+open Tactypes
 open Genredexpr
 
 open Equality
diff --git a/plugins/ltac/coretactics.ml4 b/plugins/ltac/coretactics.ml4
index faa9e413b..61525cb49 100644
--- a/plugins/ltac/coretactics.ml4
+++ b/plugins/ltac/coretactics.ml4
@@ -10,11 +10,13 @@
 
 open Util
 open Locus
-open Misctypes
+open Tactypes
 open Genredexpr
 open Stdarg
 open Extraargs
+open Tacarg
 open Names
+open Logic
 
 DECLARE PLUGIN "ltac_plugin"
 
diff --git a/plugins/ltac/evar_tactics.ml b/plugins/ltac/evar_tactics.ml
index ea8dcf57d..84f13d213 100644
--- a/plugins/ltac/evar_tactics.ml
+++ b/plugins/ltac/evar_tactics.ml
@@ -92,7 +92,7 @@ let let_evar name typ =
       Namegen.next_ident_away_in_goal id (Termops.vars_of_env env)
     | Name.Name id -> id
     in
-    let (sigma, evar) = Evarutil.new_evar env sigma ~src ~naming:(Misctypes.IntroFresh id) typ in
+    let (sigma, evar) = Evarutil.new_evar env sigma ~src ~naming:(Namegen.IntroFresh id) typ in
     Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
     (Tactics.letin_tac None (Name.Name id) evar None Locusops.nowhere)
   end
diff --git a/plugins/ltac/extraargs.ml4 b/plugins/ltac/extraargs.ml4
index 4e7c8b754..dae2582bd 100644
--- a/plugins/ltac/extraargs.ml4
+++ b/plugins/ltac/extraargs.ml4
@@ -19,7 +19,6 @@ open Tacmach
 open Tacexpr
 open Taccoerce
 open Tacinterp
-open Misctypes
 open Locus
 
 (** Adding scopes for generic arguments not defined through ARGUMENT EXTEND *)
@@ -35,7 +34,7 @@ let () = create_generic_quotation "ident" Pcoq.Prim.ident Stdarg.wit_ident
 let () = create_generic_quotation "reference" Pcoq.Prim.reference Stdarg.wit_ref
 let () = create_generic_quotation "uconstr" Pcoq.Constr.lconstr Stdarg.wit_uconstr
 let () = create_generic_quotation "constr" Pcoq.Constr.lconstr Stdarg.wit_constr
-let () = create_generic_quotation "ipattern" Pltac.simple_intropattern Stdarg.wit_intro_pattern
+let () = create_generic_quotation "ipattern" Pltac.simple_intropattern wit_intro_pattern
 let () = create_generic_quotation "open_constr" Pcoq.Constr.lconstr Stdarg.wit_open_constr
 let () =
   let inject (loc, v) = Tacexpr.Tacexp v in
diff --git a/plugins/ltac/extraargs.mli b/plugins/ltac/extraargs.mli
index ff697e3c7..737147884 100644
--- a/plugins/ltac/extraargs.mli
+++ b/plugins/ltac/extraargs.mli
@@ -12,7 +12,6 @@ open Tacexpr
 open Names
 open Constrexpr
 open Glob_term
-open Misctypes
 
 val wit_orient : bool Genarg.uniform_genarg_type
 val orient : bool Pcoq.Gram.entry
@@ -20,9 +19,9 @@ val pr_orient : bool -> Pp.t
 
 val wit_rename : (Id.t * Id.t) Genarg.uniform_genarg_type
 
-val occurrences : (int list or_var) Pcoq.Gram.entry
-val wit_occurrences : (int list or_var, int list or_var, int list) Genarg.genarg_type
-val pr_occurrences : int list or_var -> Pp.t
+val occurrences : (int list Locus.or_var) Pcoq.Gram.entry
+val wit_occurrences : (int list Locus.or_var, int list Locus.or_var, int list) Genarg.genarg_type
+val pr_occurrences : int list Locus.or_var -> Pp.t
 val occurrences_of : int list -> Locus.occurrences
 
 val wit_natural : int Genarg.uniform_genarg_type
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index cb7183638..f2899ab63 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -24,7 +24,8 @@ open CErrors
 open Util
 open Termops
 open Equality
-open Misctypes
+open Namegen
+open Tactypes
 open Proofview.Notations
 open Vernacinterp
 
@@ -604,7 +605,7 @@ let subst_var_with_hole occ tid t =
 	     (incr locref;
               DAst.make ~loc:(Loc.make_loc (!locref,0)) @@
 	      GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true,Anonymous),
-                     Misctypes.IntroAnonymous, None)))
+                     IntroAnonymous, None)))
         else x
     | _ -> map_glob_constr_left_to_right substrec x in
   let t' = substrec t
@@ -615,13 +616,13 @@ let subst_hole_with_term occ tc t =
   let locref = ref 0 in
   let occref = ref occ in
   let rec substrec c = match DAst.get c with
-    | GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true,Anonymous),Misctypes.IntroAnonymous,s) ->
+    | GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true,Anonymous),IntroAnonymous,s) ->
         decr occref;
         if Int.equal !occref 0 then tc
         else
 	  (incr locref;
            DAst.make ~loc:(Loc.make_loc (!locref,0)) @@
-	   GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true,Anonymous),Misctypes.IntroAnonymous,s))
+           GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true,Anonymous),IntroAnonymous,s))
     | _ -> map_glob_constr_left_to_right substrec c
   in
   substrec t
diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4
index ed54320a5..d7d642e50 100644
--- a/plugins/ltac/g_ltac.ml4
+++ b/plugins/ltac/g_ltac.ml4
@@ -12,9 +12,10 @@ DECLARE PLUGIN "ltac_plugin"
 
 open Util
 open Pp
+open Glob_term
 open Constrexpr
 open Tacexpr
-open Misctypes
+open Namegen
 open Genarg
 open Genredexpr
 open Tok (* necessary for camlp5 *)
@@ -26,7 +27,7 @@ open Pcoq.Constr
 open Pvernac.Vernac_
 open Pltac
 
-let fail_default_value = ArgArg 0
+let fail_default_value = Locus.ArgArg 0
 
 let arg_of_expr = function
     TacArg (loc,a) -> a
@@ -34,7 +35,7 @@ let arg_of_expr = function
 
 let genarg_of_unit () = in_gen (rawwit Stdarg.wit_unit) ()
 let genarg_of_int n = in_gen (rawwit Stdarg.wit_int) n
-let genarg_of_ipattern pat = in_gen (rawwit Stdarg.wit_intro_pattern) pat
+let genarg_of_ipattern pat = in_gen (rawwit Tacarg.wit_intro_pattern) pat
 let genarg_of_uconstr c = in_gen (rawwit Stdarg.wit_uconstr) c
 let in_tac tac = in_gen (rawwit Tacarg.wit_ltac) tac
 
@@ -197,9 +198,9 @@ GEXTEND Gram
      non ambiguous name where dots are replaced by "_"? Probably too
      verbose most of the time. *)
   fresh_id:
-    [ [ s = STRING -> ArgArg s (*| id = ident -> ArgVar (!@loc,id)*)
+    [ [ s = STRING -> Locus.ArgArg s (*| id = ident -> Locus.ArgVar (!@loc,id)*)
         | qid = qualid -> let (_pth,id) = Libnames.repr_qualid qid.CAst.v in
-                          ArgVar (CAst.make ~loc:!@loc id) ] ]
+                          Locus.ArgVar (CAst.make ~loc:!@loc id) ] ]
   ;
   constr_eval:
     [ [ IDENT "eval"; rtc = red_expr; "in"; c = Constr.constr ->
diff --git a/plugins/ltac/g_rewrite.ml4 b/plugins/ltac/g_rewrite.ml4
index 079001ee4..2189e224f 100644
--- a/plugins/ltac/g_rewrite.ml4
+++ b/plugins/ltac/g_rewrite.ml4
@@ -11,7 +11,6 @@
 (* Syntax for rewriting with strategies *)
 
 open Names
-open Misctypes
 open Locus
 open Constrexpr
 open Glob_term
@@ -20,6 +19,7 @@ open Extraargs
 open Tacmach
 open Rewrite
 open Stdarg
+open Tactypes
 open Pcoq.Prim
 open Pcoq.Constr
 open Pvernac.Vernac_
diff --git a/plugins/ltac/g_tactic.ml4 b/plugins/ltac/g_tactic.ml4
index dc9f607cf..05005c733 100644
--- a/plugins/ltac/g_tactic.ml4
+++ b/plugins/ltac/g_tactic.ml4
@@ -11,12 +11,14 @@
 open Pp
 open CErrors
 open Util
+open Names
+open Namegen
 open Tacexpr
 open Genredexpr
 open Constrexpr
 open Libnames
 open Tok
-open Misctypes
+open Tactypes
 open Locus
 open Decl_kinds
 
@@ -383,19 +385,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:
@@ -494,12 +496,12 @@ GEXTEND Gram
     | -> None ] ]
   ;
   rewriter :
-    [ [ "!"; c = constr_with_bindings_arg -> (RepeatPlus,c)
-      | ["?"| LEFTQMARK]; c = constr_with_bindings_arg -> (RepeatStar,c)
-      | n = natural; "!"; c = constr_with_bindings_arg -> (Precisely n,c)
-      |	n = natural; ["?" | LEFTQMARK]; c = constr_with_bindings_arg -> (UpTo n,c)
-      | n = natural; c = constr_with_bindings_arg -> (Precisely n,c)
-      | c = constr_with_bindings_arg -> (Precisely 1, c)
+    [ [ "!"; c = constr_with_bindings_arg -> (Equality.RepeatPlus,c)
+      | ["?"| LEFTQMARK]; c = constr_with_bindings_arg -> (Equality.RepeatStar,c)
+      | n = natural; "!"; c = constr_with_bindings_arg -> (Equality.Precisely n,c)
+      |	n = natural; ["?" | LEFTQMARK]; c = constr_with_bindings_arg -> (Equality.UpTo n,c)
+      | n = natural; c = constr_with_bindings_arg -> (Equality.Precisely n,c)
+      | c = constr_with_bindings_arg -> (Equality.Precisely 1, c)
       ] ]
   ;
   oriented_rewriter :
diff --git a/plugins/ltac/pltac.mli b/plugins/ltac/pltac.mli
index 434feba95..4c075d413 100644
--- a/plugins/ltac/pltac.mli
+++ b/plugins/ltac/pltac.mli
@@ -15,22 +15,22 @@ open Libnames
 open Constrexpr
 open Tacexpr
 open Genredexpr
-open Misctypes
+open Tactypes
 
 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
 val quantified_hypothesis : quantified_hypothesis Gram.entry
 val destruction_arg : constr_expr with_bindings Tactics.destruction_arg Gram.entry
-val int_or_var : int or_var Gram.entry
+val int_or_var : int Locus.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/pptactic.ml b/plugins/ltac/pptactic.ml
index b29af6680..e19a95e84 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -19,7 +19,7 @@ open Geninterp
 open Stdarg
 open Libnames
 open Notation_gram
-open Misctypes
+open Tactypes
 open Locus
 open Decl_kinds
 open Genredexpr
@@ -493,7 +493,7 @@ let string_of_genarg_arg (ArgumentType arg) =
 
   let pr_orient b = if b then mt () else str "<- "
 
-  let pr_multi = function
+  let pr_multi = let open Equality in function
     | Precisely 1 -> mt ()
     | Precisely n -> int n ++ str "!"
     | UpTo n -> int n ++ str "?"
@@ -749,7 +749,7 @@ let pr_goal_selector ~toplevel s =
         | TacIntroPattern (ev,(_::_ as p)) ->
            hov 1 (primitive (if ev then "eintros" else "intros") ++
                     (match p with
-                    | [{CAst.v=Misctypes.IntroForthcoming false}] -> mt ()
+                    | [{CAst.v=IntroForthcoming false}] -> mt ()
                     | _ -> spc () ++ prlist_with_sep spc (Miscprint.pr_intro_pattern pr.pr_dconstr) p))
         | TacApply (a,ev,cb,inhyp) ->
           hov 1 (
diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli
index 5d2a99618..6c09e447a 100644
--- a/plugins/ltac/pptactic.mli
+++ b/plugins/ltac/pptactic.mli
@@ -14,11 +14,11 @@
 open Genarg
 open Geninterp
 open Names
-open Misctypes
 open Environ
 open Constrexpr
 open Notation_gram
 open Tacexpr
+open Tactypes
 
 type 'a grammar_tactic_prod_item_expr =
 | TacTerm of string
@@ -97,7 +97,7 @@ val pr_may_eval :
   ('a -> Pp.t) -> ('a -> Pp.t) -> ('b -> Pp.t) ->
   ('c -> Pp.t) -> ('a,'b,'c) Genredexpr.may_eval -> Pp.t
 
-val pr_and_short_name : ('a -> Pp.t) -> 'a and_short_name -> Pp.t
+val pr_and_short_name : ('a -> Pp.t) -> 'a Stdarg.and_short_name -> Pp.t
 val pr_or_by_notation : ('a -> Pp.t) -> 'a or_by_notation -> Pp.t
 
 val pr_evaluable_reference_env : env -> evaluable_global_reference -> Pp.t
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index b91315aca..cd04f4ae9 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -26,7 +26,7 @@ open Classes
 open Constrexpr
 open Globnames
 open Evd
-open Misctypes
+open Tactypes
 open Locus
 open Locusops
 open Decl_kinds
@@ -1846,7 +1846,7 @@ let declare_relation ?locality ?(binders=[]) a aeq n refl symm trans =
              (CAst.make @@ Ident (Id.of_string "Equivalence_Symmetric"), lemma2);
              (CAst.make @@ Ident (Id.of_string "Equivalence_Transitive"), lemma3)])
 
-let cHole = CAst.make @@ CHole (None, Misctypes.IntroAnonymous, None)
+let cHole = CAst.make @@ CHole (None, Namegen.IntroAnonymous, None)
 
 let proper_projection sigma r ty =
   let rel_vect n m = Array.init m (fun i -> mkRel(n+m-i)) in
diff --git a/plugins/ltac/rewrite.mli b/plugins/ltac/rewrite.mli
index 1e3d4733b..0d014a0bf 100644
--- a/plugins/ltac/rewrite.mli
+++ b/plugins/ltac/rewrite.mli
@@ -12,9 +12,9 @@ open Names
 open Environ
 open EConstr
 open Constrexpr
-open Tacexpr
-open Misctypes
 open Evd
+open Tactypes
+open Tacexpr
 open Tacinterp
 
 (** TODO: document and clean me! *)
diff --git a/plugins/ltac/tacarg.ml b/plugins/ltac/tacarg.ml
index 6eb482b1c..8a25d4851 100644
--- a/plugins/ltac/tacarg.ml
+++ b/plugins/ltac/tacarg.ml
@@ -19,6 +19,14 @@ let make0 ?dyn name =
   let () = Geninterp.register_val0 wit dyn in
   wit
 
+let wit_intro_pattern = make0 "intropattern"
+let wit_quant_hyp = make0 "quant_hyp"
+let wit_constr_with_bindings = make0 "constr_with_bindings"
+let wit_open_constr_with_bindings = make0 "open_constr_with_bindings"
+let wit_bindings = make0 "bindings"
+let wit_quantified_hypothesis = wit_quant_hyp
+let wit_intropattern = wit_intro_pattern
+
 let wit_tactic : (raw_tactic_expr, glob_tactic_expr, Val.t) genarg_type =
   make0 "tactic"
 
diff --git a/plugins/ltac/tacarg.mli b/plugins/ltac/tacarg.mli
index 59473a5e5..bdb0be03c 100644
--- a/plugins/ltac/tacarg.mli
+++ b/plugins/ltac/tacarg.mli
@@ -9,9 +9,33 @@
 (************************************************************************)
 
 open Genarg
-open Tacexpr
+open EConstr
 open Constrexpr
-open Misctypes
+open Tactypes
+open Tacexpr
+
+(** Tactic related witnesses, could also live in tactics/ if other users *)
+val wit_intro_pattern : (constr_expr intro_pattern_expr CAst.t, glob_constr_and_expr intro_pattern_expr CAst.t, intro_pattern) genarg_type
+
+val wit_quant_hyp : quantified_hypothesis uniform_genarg_type
+
+val wit_constr_with_bindings :
+  (constr_expr with_bindings,
+  glob_constr_and_expr with_bindings,
+  constr with_bindings delayed_open) genarg_type
+
+val wit_open_constr_with_bindings :
+  (constr_expr with_bindings,
+  glob_constr_and_expr with_bindings,
+  constr with_bindings delayed_open) genarg_type
+
+val wit_bindings :
+  (constr_expr bindings,
+  glob_constr_and_expr bindings,
+  constr bindings delayed_open) genarg_type
+
+val wit_quantified_hypothesis : quantified_hypothesis uniform_genarg_type
+val wit_intropattern : (constr_expr intro_pattern_expr CAst.t, glob_constr_and_expr intro_pattern_expr CAst.t, intro_pattern) genarg_type
 
 (** Generic arguments based on Ltac. *)
 
diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml
index 3812a2ba2..cc9c2046d 100644
--- a/plugins/ltac/taccoerce.ml
+++ b/plugins/ltac/taccoerce.ml
@@ -12,9 +12,11 @@ open Util
 open Names
 open Constr
 open EConstr
-open Misctypes
+open Namegen
+open Tactypes
 open Genarg
 open Stdarg
+open Tacarg
 open Geninterp
 open Pp
 
@@ -365,7 +367,7 @@ let coerce_to_int_or_var_list v =
   match Value.to_list v with
   | None -> raise (CannotCoerceTo "an int list")
   | Some l ->
-    let map n = ArgArg (coerce_to_int n) in
+    let map n = Locus.ArgArg (coerce_to_int n) in
     List.map map l
 
 (** Abstract application, to print ltac functions *)
diff --git a/plugins/ltac/taccoerce.mli b/plugins/ltac/taccoerce.mli
index 5185217cd..56f881684 100644
--- a/plugins/ltac/taccoerce.mli
+++ b/plugins/ltac/taccoerce.mli
@@ -11,9 +11,9 @@
 open Util
 open Names
 open EConstr
-open Misctypes
 open Genarg
 open Geninterp
+open Tactypes
 
 (** Coercions from highest level generic arguments to actual data used by Ltac
     interpretation. Those functions examinate dynamic types and try to return
@@ -56,7 +56,7 @@ val coerce_to_ident_not_fresh : Environ.env -> Evd.evar_map -> Value.t -> Id.t
 val coerce_to_intro_pattern : Environ.env -> Evd.evar_map -> Value.t -> Tacexpr.delayed_open_constr intro_pattern_expr
 
 val coerce_to_intro_pattern_naming :
-  Environ.env -> Evd.evar_map -> Value.t -> intro_pattern_naming_expr
+  Environ.env -> Evd.evar_map -> Value.t -> Namegen.intro_pattern_naming_expr
 
 val coerce_to_hint_base : Value.t -> string
 
@@ -86,7 +86,7 @@ val coerce_to_quantified_hypothesis : Evd.evar_map -> Value.t -> quantified_hypo
 
 val coerce_to_decl_or_quant_hyp : Environ.env -> Evd.evar_map -> Value.t -> quantified_hypothesis
 
-val coerce_to_int_or_var_list : Value.t -> int or_var list
+val coerce_to_int_or_var_list : Value.t -> int Locus.or_var list
 
 (** {5 Missing generic arguments} *)
 
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index e510b9f59..fada7424c 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -376,7 +376,7 @@ let add_ml_tactic_notation name ~level prods =
     in
     let ids = List.map_filter get_id prods in
     let entry = { mltac_name = name; mltac_index = len - i - 1 } in
-    let map id = Reference (Misctypes.ArgVar (CAst.make id)) in
+    let map id = Reference (Locus.ArgVar (CAst.make id)) in
     let tac = TacML (Loc.tag (entry, List.map map ids)) in
     add_glob_tactic_notation false ~level prods true ids tac
   in
diff --git a/plugins/ltac/tacexpr.ml b/plugins/ltac/tacexpr.ml
index 17f5e5d41..d51de8c65 100644
--- a/plugins/ltac/tacexpr.ml
+++ b/plugins/ltac/tacexpr.ml
@@ -15,7 +15,7 @@ open Libnames
 open Genredexpr
 open Genarg
 open Pattern
-open Misctypes
+open Tactypes
 open Locus
 
 type ltac_constant = KerName.t
@@ -75,7 +75,7 @@ type 'id message_token =
 
 type ('dconstr,'id) induction_clause =
     'dconstr with_bindings Tactics.destruction_arg *
-    (intro_pattern_naming_expr CAst.t option (* eqn:... *)
+    (Namegen.intro_pattern_naming_expr CAst.t option (* eqn:... *)
     * 'dconstr or_and_intro_pattern_expr CAst.t or_var option) (* as ... *)
     * 'id clause_expr option (* in ... *)
 
@@ -117,7 +117,7 @@ type ml_tactic_entry = {
 
 (** Composite types *)
 
-type glob_constr_and_expr = Tactypes.glob_constr_and_expr
+type glob_constr_and_expr = Genintern.glob_constr_and_expr
 
 type open_constr_expr = unit * constr_expr
 type open_glob_constr = unit * glob_constr_and_expr
@@ -134,7 +134,7 @@ type delayed_open_constr = EConstr.constr delayed_open
 type intro_pattern = delayed_open_constr intro_pattern_expr CAst.t
 type intro_patterns = delayed_open_constr intro_pattern_expr CAst.t list
 type or_and_intro_pattern = delayed_open_constr or_and_intro_pattern_expr CAst.t
-type intro_pattern_naming = intro_pattern_naming_expr CAst.t
+type intro_pattern_naming = Namegen.intro_pattern_naming_expr CAst.t
 
 (** Generic expressions for atomic tactics *)
 
@@ -152,7 +152,7 @@ type 'a gen_atomic_tactic_expr =
       'dtrm intro_pattern_expr CAst.t option * 'trm
   | TacGeneralize of ('trm with_occurrences * Name.t) list
   | TacLetTac of evars_flag * Name.t * 'trm * 'nam clause_expr * letin_flag *
-      intro_pattern_naming_expr CAst.t option
+      Namegen.intro_pattern_naming_expr CAst.t option
 
   (* Derived basic tactics *)
   | TacInductionDestruct of
@@ -164,7 +164,7 @@ type 'a gen_atomic_tactic_expr =
 
   (* Equality and inversion *)
   | TacRewrite of evars_flag *
-      (bool * multi * 'dtrm with_bindings_arg) list * 'nam clause_expr *
+      (bool * Equality.multi * 'dtrm with_bindings_arg) list * 'nam clause_expr *
       (* spiwack: using ['dtrm] here is a small hack, may not be
          stable by a change in the representation of delayed
          terms. Because, in fact, it is the whole "with_bindings"
@@ -305,7 +305,7 @@ constraint 'a = <
 
 type g_trm = glob_constr_and_expr
 type g_pat = glob_constr_pattern_and_expr
-type g_cst = evaluable_global_reference and_short_name or_var
+type g_cst = evaluable_global_reference Stdarg.and_short_name or_var
 type g_ref = ltac_constant located or_var
 type g_nam = lident
 
diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli
index 17f5e5d41..01eead164 100644
--- a/plugins/ltac/tacexpr.mli
+++ b/plugins/ltac/tacexpr.mli
@@ -15,8 +15,8 @@ open Libnames
 open Genredexpr
 open Genarg
 open Pattern
-open Misctypes
 open Locus
+open Tactypes
 
 type ltac_constant = KerName.t
 
@@ -75,7 +75,7 @@ type 'id message_token =
 
 type ('dconstr,'id) induction_clause =
     'dconstr with_bindings Tactics.destruction_arg *
-    (intro_pattern_naming_expr CAst.t option (* eqn:... *)
+    (Namegen.intro_pattern_naming_expr CAst.t option (* eqn:... *)
     * 'dconstr or_and_intro_pattern_expr CAst.t or_var option) (* as ... *)
     * 'id clause_expr option (* in ... *)
 
@@ -117,7 +117,7 @@ type ml_tactic_entry = {
 
 (** Composite types *)
 
-type glob_constr_and_expr = Tactypes.glob_constr_and_expr
+type glob_constr_and_expr = Genintern.glob_constr_and_expr
 
 type open_constr_expr = unit * constr_expr
 type open_glob_constr = unit * glob_constr_and_expr
@@ -134,7 +134,7 @@ type delayed_open_constr = EConstr.constr delayed_open
 type intro_pattern = delayed_open_constr intro_pattern_expr CAst.t
 type intro_patterns = delayed_open_constr intro_pattern_expr CAst.t list
 type or_and_intro_pattern = delayed_open_constr or_and_intro_pattern_expr CAst.t
-type intro_pattern_naming = intro_pattern_naming_expr CAst.t
+type intro_pattern_naming = Namegen.intro_pattern_naming_expr CAst.t
 
 (** Generic expressions for atomic tactics *)
 
@@ -152,7 +152,7 @@ type 'a gen_atomic_tactic_expr =
       'dtrm intro_pattern_expr CAst.t option * 'trm
   | TacGeneralize of ('trm with_occurrences * Name.t) list
   | TacLetTac of evars_flag * Name.t * 'trm * 'nam clause_expr * letin_flag *
-      intro_pattern_naming_expr CAst.t option
+      Namegen.intro_pattern_naming_expr CAst.t option
 
   (* Derived basic tactics *)
   | TacInductionDestruct of
@@ -164,7 +164,7 @@ type 'a gen_atomic_tactic_expr =
 
   (* Equality and inversion *)
   | TacRewrite of evars_flag *
-      (bool * multi * 'dtrm with_bindings_arg) list * 'nam clause_expr *
+      (bool * Equality.multi * 'dtrm with_bindings_arg) list * 'nam clause_expr *
       (* spiwack: using ['dtrm] here is a small hack, may not be
          stable by a change in the representation of delayed
          terms. Because, in fact, it is the whole "with_bindings"
@@ -305,7 +305,7 @@ constraint 'a = <
 
 type g_trm = glob_constr_and_expr
 type g_pat = glob_constr_pattern_and_expr
-type g_cst = evaluable_global_reference and_short_name or_var
+type g_cst = evaluable_global_reference Stdarg.and_short_name or_var
 type g_ref = ltac_constant located or_var
 type g_nam = lident
 
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index 9ad9e1520..cef5bb1b8 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -27,7 +27,8 @@ open Tacexpr
 open Genarg
 open Stdarg
 open Tacarg
-open Misctypes
+open Namegen
+open Tactypes
 open Locus
 
 (** Globalization of tactic expressions :
diff --git a/plugins/ltac/tacintern.mli b/plugins/ltac/tacintern.mli
index fb32508cc..9146fced2 100644
--- a/plugins/ltac/tacintern.mli
+++ b/plugins/ltac/tacintern.mli
@@ -12,7 +12,7 @@ open Names
 open Tacexpr
 open Genarg
 open Constrexpr
-open Misctypes
+open Tactypes
 
 (** Globalization of tactic expressions :
     Conversion from [raw_tactic_expr] to [glob_tactic_expr] *)
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index a93cf5ae7..8a8f9e71a 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -12,6 +12,7 @@ open Constrintern
 open Patternops
 open Pp
 open CAst
+open Namegen
 open Genredexpr
 open Glob_term
 open Glob_ops
@@ -35,7 +36,7 @@ open Stdarg
 open Tacarg
 open Printer
 open Pretyping
-open Misctypes
+open Tactypes
 open Locus
 open Tacintern
 open Taccoerce
diff --git a/plugins/ltac/tacinterp.mli b/plugins/ltac/tacinterp.mli
index bd44bdbea..fd2d96bd6 100644
--- a/plugins/ltac/tacinterp.mli
+++ b/plugins/ltac/tacinterp.mli
@@ -14,7 +14,7 @@ open EConstr
 open Tacexpr
 open Genarg
 open Redexpr
-open Misctypes
+open Tactypes
 
 val ltac_trace_info : ltac_trace Exninfo.t
 
@@ -131,7 +131,7 @@ val interp_ltac_var : (value -> 'a) -> interp_sign ->
 
 val interp_int : interp_sign -> lident -> int
 
-val interp_int_or_var : interp_sign -> int or_var -> int
+val interp_int_or_var : interp_sign -> int Locus.or_var -> int
 
 val default_ist : unit -> Geninterp.interp_sign
 (** Empty ist with debug set on the current value. *)
diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml
index 50bf687b1..dd799dc13 100644
--- a/plugins/ltac/tacsubst.ml
+++ b/plugins/ltac/tacsubst.ml
@@ -14,7 +14,7 @@ open Mod_subst
 open Genarg
 open Stdarg
 open Tacarg
-open Misctypes
+open Tactypes
 open Globnames
 open Genredexpr
 open Patternops
@@ -75,7 +75,7 @@ let subst_and_short_name f (c,n) =
 (*  assert (n=None); *)(* since tacdef are strictly globalized *)
   (f c,None)
 
-let subst_or_var f =  function
+let subst_or_var f =  let open Locus in function
   | ArgVar _ as x -> x
   | ArgArg x -> ArgArg (f x)
 
diff --git a/plugins/ltac/tacsubst.mli b/plugins/ltac/tacsubst.mli
index 0a894791b..d406686c5 100644
--- a/plugins/ltac/tacsubst.mli
+++ b/plugins/ltac/tacsubst.mli
@@ -11,7 +11,7 @@
 open Tacexpr
 open Mod_subst
 open Genarg
-open Misctypes
+open Tactypes
 
 (** Substitution of tactics at module closing time *)
 
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/plugins/ltac/tauto.ml b/plugins/ltac/tauto.ml
index 8eeb8903e..299bc7ea4 100644
--- a/plugins/ltac/tauto.ml
+++ b/plugins/ltac/tauto.ml
@@ -13,7 +13,6 @@ open EConstr
 open Hipattern
 open Names
 open Geninterp
-open Misctypes
 open Ltac_plugin
 open Tacexpr
 open Tacinterp
@@ -94,7 +93,7 @@ let clear id = Tactics.clear [id]
 
 let assumption = Tactics.assumption
 
-let split = Tactics.split_with_bindings false [Misctypes.NoBindings]
+let split = Tactics.split_with_bindings false [Tactypes.NoBindings]
 
 (** Test *)
 
@@ -175,7 +174,7 @@ let flatten_contravariant_disj _ ist =
   | Some (_,args) ->
       let map i arg =
         let typ = mkArrow arg c in
-        let ci = Tactics.constructor_tac false None (succ i) Misctypes.NoBindings in
+        let ci = Tactics.constructor_tac false None (succ i) Tactypes.NoBindings in
         let by = tclTHENLIST [intro; apply hyp; ci; assumption] in
         assert_ ~by typ
       in
@@ -187,7 +186,7 @@ let flatten_contravariant_disj _ ist =
 let make_unfold name =
   let dir = DirPath.make (List.map Id.of_string ["Logic"; "Init"; "Coq"]) in
   let const = Constant.make2 (ModPath.MPfile dir) (Label.make name) in
-  (Locus.AllOccurrences, ArgArg (EvalConstRef const, None))
+  Locus.(AllOccurrences, ArgArg (EvalConstRef const, None))
 
 let u_not = make_unfold "not"
 
@@ -245,7 +244,7 @@ let with_flags flags _ ist =
   let x = CAst.make @@ Id.of_string "x" in
   let arg = Val.Dyn (tag_tauto_flags, flags) in
   let ist = { ist with lfun = Id.Map.add x.CAst.v arg ist.lfun } in
-  eval_tactic_ist ist (TacArg (Loc.tag @@ TacCall (Loc.tag (ArgVar f, [Reference (ArgVar x)]))))
+  eval_tactic_ist ist (TacArg (Loc.tag @@ TacCall (Loc.tag (Locus.ArgVar f, [Reference (Locus.ArgVar x)]))))
 
 let register_tauto_tactic tac name0 args =
   let ids = List.map (fun id -> Id.of_string id) args in
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index 68620dbfc..f22147f8b 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -23,6 +23,7 @@ open Names
 open Goptions
 open Mutils
 open Constr
+open Tactypes
 
 (**
   * Debug flag 
@@ -1727,7 +1728,7 @@ let micromega_gen
 
        let intro_vars = Tacticals.New.tclTHENLIST (List.map intro vars) in
        let intro_props = Tacticals.New.tclTHENLIST (List.map intro props) in
-       let ipat_of_name id = Some (CAst.make @@ Misctypes.IntroNaming (Misctypes.IntroIdentifier id)) in
+       let ipat_of_name id = Some (CAst.make @@ IntroNaming (Namegen.IntroIdentifier id)) in
        let goal_name = fresh_id Id.Set.empty (Names.Id.of_string "__arith") gl in
        let env' = List.map (fun (id,i) -> EConstr.mkVar id,i) vars in 
 
@@ -1842,7 +1843,7 @@ let micromega_genr prover tac =
 
        let intro_vars = Tacticals.New.tclTHENLIST (List.map intro vars) in
        let intro_props = Tacticals.New.tclTHENLIST (List.map intro props) in
-       let ipat_of_name id = Some (CAst.make @@ Misctypes.IntroNaming (Misctypes.IntroIdentifier id)) in
+       let ipat_of_name id = Some (CAst.make @@ IntroNaming (Namegen.IntroIdentifier id)) in
        let goal_name = fresh_id Id.Set.empty (Names.Id.of_string "__arith") gl in
        let env' = List.map (fun (id,i) -> EConstr.mkVar id,i) vars in 
        
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index c615cf278..6f4138828 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -29,7 +29,7 @@ open Libnames
 open Globnames
 open Nametab
 open Contradiction
-open Misctypes
+open Tactypes
 open Context.Named.Declaration
 
 module NamedDecl = Context.Named.Declaration
diff --git a/plugins/quote/g_quote.ml4 b/plugins/quote/g_quote.ml4
index c35e0fe12..09209dc22 100644
--- a/plugins/quote/g_quote.ml4
+++ b/plugins/quote/g_quote.ml4
@@ -10,7 +10,6 @@
 
 open Ltac_plugin
 open Names
-open Misctypes
 open Tacexpr
 open Geninterp
 open Quote
@@ -24,7 +23,7 @@ let x = Id.of_string "x"
 
 let make_cont (k : Val.t) (c : EConstr.t) =
   let c = Tacinterp.Value.of_constr c in
-  let tac = TacCall (Loc.tag (ArgVar CAst.(make cont), [Reference (ArgVar CAst.(make x))])) in
+  let tac = TacCall (Loc.tag (Locus.ArgVar CAst.(make cont), [Reference (Locus.ArgVar CAst.(make x))])) in
   let ist = { lfun = Id.Map.add cont k (Id.Map.singleton x c); extra = TacStore.empty; } in
   Tacinterp.eval_tactic_ist ist (TacArg (Loc.tag tac))
 
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index b9d0d2e25..84b29a0bf 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -20,6 +20,7 @@ open Environ
 open Libnames
 open Globnames
 open Glob_term
+open Locus
 open Tacexpr
 open Coqlib
 open Mod_subst
@@ -29,7 +30,6 @@ open Printer
 open Declare
 open Decl_kinds
 open Entries
-open Misctypes
 open Newring_ast
 open Proofview.Notations
 
diff --git a/plugins/ssr/ssrast.mli b/plugins/ssr/ssrast.mli
index 7f5f2f63d..5571c5420 100644
--- a/plugins/ssr/ssrast.mli
+++ b/plugins/ssr/ssrast.mli
@@ -37,7 +37,7 @@ type ssrmult = int * ssrmmod
 type ssrocc = (bool * int list) option
 
 (* index MAYBE REMOVE ONLY INTERNAL stuff between {} *)
-type ssrindex = int Misctypes.or_var
+type ssrindex = int Locus.or_var
 
 (* clear switch {H G} *)
 type ssrclear = ssrhyps
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index 3f6503e73..2a31157be 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -181,10 +181,9 @@ let option_assert_get o msg =
 (** Constructors for rawconstr *)
 open Glob_term
 open Globnames
-open Misctypes
 open Decl_kinds
 
-let mkRHole = DAst.make @@ GHole (Evar_kinds.InternalHole, IntroAnonymous, None)
+let mkRHole = DAst.make @@ GHole (Evar_kinds.InternalHole, Namegen.IntroAnonymous, None)
 
 let rec mkRHoles n = if n > 0 then mkRHole :: mkRHoles (n - 1) else []
 let rec isRHoles cl = match cl with
@@ -254,7 +253,7 @@ let interp_refine ist gl rc =
 
 
 let interp_open_constr ist gl gc =
-  let (sigma, (c, _)) = Tacinterp.interp_open_constr_with_bindings ist (pf_env gl) (project gl) (gc, Misctypes.NoBindings) in
+  let (sigma, (c, _)) = Tacinterp.interp_open_constr_with_bindings ist (pf_env gl) (project gl) (gc, Tactypes.NoBindings) in
   (project gl, (sigma, c))
 
 let interp_term ist gl (_, c) = snd (interp_open_constr ist gl c)
@@ -861,8 +860,8 @@ let mkCProp loc = CAst.make ?loc @@ CSort GProp
 let mkCType loc = CAst.make ?loc @@ CSort (GType [])
 let mkCVar ?loc id = CAst.make ?loc @@ CRef (CAst.make ?loc @@ Ident id, None)
 let rec mkCHoles ?loc n =
-  if n <= 0 then [] else (CAst.make ?loc @@ CHole (None, IntroAnonymous, None)) :: mkCHoles ?loc (n - 1)
-let mkCHole loc = CAst.make ?loc @@ CHole (None, IntroAnonymous, None)
+  if n <= 0 then [] else (CAst.make ?loc @@ CHole (None, Namegen.IntroAnonymous, None)) :: mkCHoles ?loc (n - 1)
+let mkCHole loc = CAst.make ?loc @@ CHole (None, Namegen.IntroAnonymous, None)
 let mkCLambda ?loc name ty t =  CAst.make ?loc @@
    CLambdaN ([CLocalAssum([CAst.make ?loc name], Default Explicit, ty)], t)
 let mkCArrow ?loc ty t = CAst.make ?loc @@
diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml
index 83b4d6562..fbe3b000f 100644
--- a/plugins/ssr/ssrelim.ml
+++ b/plugins/ssr/ssrelim.ml
@@ -17,7 +17,7 @@ open Term
 open Constr
 open Termops
 open Globnames
-open Misctypes
+open Tactypes
 open Tacmach
 
 open Ssrmatching_plugin
diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml
index c6beb08c5..2c046190f 100644
--- a/plugins/ssr/ssrfwd.ml
+++ b/plugins/ssr/ssrfwd.ml
@@ -86,7 +86,6 @@ let _ =
 
 open Constrexpr 
 open Glob_term 
-open Misctypes
 
 let combineCG t1 t2 f g = match t1, t2 with
  | (x, (t1, None)), (_, (t2, None)) -> x, (g t1 t2, None)
diff --git a/plugins/ssr/ssrparser.ml4 b/plugins/ssr/ssrparser.ml4
index fbfbdb110..352f88bb3 100644
--- a/plugins/ssr/ssrparser.ml4
+++ b/plugins/ssr/ssrparser.ml4
@@ -22,13 +22,15 @@ open Libnames
 open Tactics
 open Tacmach
 open Util
+open Locus
 open Tacexpr
 open Tacinterp
 open Pltac
 open Extraargs
 open Ppconstr
 
-open Misctypes
+open Namegen
+open Tactypes
 open Decl_kinds
 open Constrexpr
 open Constrexpr_ops
@@ -301,24 +303,24 @@ END
 
 
 let pr_index = function
-  | Misctypes.ArgVar {CAst.v=id} -> pr_id id
-  | Misctypes.ArgArg n when n > 0 -> int n
+  | ArgVar {CAst.v=id} -> pr_id id
+  | ArgArg n when n > 0 -> int n
   | _ -> mt ()
 let pr_ssrindex _ _ _ = pr_index
 
-let noindex = Misctypes.ArgArg 0
+let noindex = ArgArg 0
 
 let check_index ?loc i =
   if i > 0 then i else CErrors.user_err ?loc (str"Index not positive")
 let mk_index ?loc = function
-  | Misctypes.ArgArg i -> Misctypes.ArgArg (check_index ?loc i)
+  | ArgArg i -> ArgArg (check_index ?loc i)
   | iv -> iv
 
 let interp_index ist gl idx =
   Tacmach.project gl,
   match idx with
-  | Misctypes.ArgArg _ -> idx
-  | Misctypes.ArgVar id ->
+  | ArgArg _ -> idx
+  | ArgVar id ->
     let i =
       try
         let v = Id.Map.find id.CAst.v ist.Tacinterp.lfun in
@@ -336,7 +338,7 @@ let interp_index ist gl idx =
         | None -> raise Not_found
         end end
     with _ -> CErrors.user_err ?loc:id.CAst.loc (str"Index not a number") in
-    Misctypes.ArgArg (check_index ?loc:id.CAst.loc i)
+    ArgArg (check_index ?loc:id.CAst.loc i)
 
 open Pltac
 
@@ -543,7 +545,7 @@ END
 
 let remove_loc x = x.CAst.v
 
-let ipat_of_intro_pattern p = Misctypes.(
+let ipat_of_intro_pattern p = Tactypes.(
   let rec ipat_of_intro_pattern = function
     | IntroNaming (IntroIdentifier id) -> IPatId id
     | IntroAction IntroWildcard -> IPatAnon Drop
@@ -595,16 +597,15 @@ let intern_ipats ist = List.map (intern_ipat ist)
 
 let interp_intro_pattern = interp_wit wit_intro_pattern
 
-let interp_introid ist gl id = Misctypes.(
+let interp_introid ist gl id =
  try IntroNaming (IntroIdentifier (hyp_id (snd (interp_hyp ist gl (SsrHyp (Loc.tag id))))))
  with _ -> (snd (interp_intro_pattern ist gl (CAst.make @@ IntroNaming (IntroIdentifier id)))).CAst.v
-)
 
 let get_intro_id = function
   | IntroNaming (IntroIdentifier id) -> id
   | _ -> assert false
 
-let rec add_intro_pattern_hyps ipat hyps = Misctypes.(
+let rec add_intro_pattern_hyps ipat hyps =
   let {CAst.loc=loc;v=ipat} = ipat in
   match ipat with
   | IntroNaming (IntroIdentifier id) ->
@@ -623,7 +624,6 @@ let rec add_intro_pattern_hyps ipat hyps = Misctypes.(
   | IntroForthcoming _ -> 
     (* As in ipat_of_intro_pattern, was unable to determine which kind
       of ipat interp_introid could return [HH] *) assert false
-)
 
 (* We interp the ipat using the standard ltac machinery for ids, since
  * we have no clue what a name could be bound to (maybe another ipat) *)
@@ -1064,7 +1064,7 @@ let rec format_constr_expr h0 c0 = let open CAst in match h0, c0 with
   | BFdef :: h, { v = CLetIn({CAst.v=x}, v, oty, c) } ->
     let bs, c' = format_constr_expr h c in
     Bdef (x, oty, v) :: bs, c'
-  | [BFcast], { v = CCast (c, CastConv t) } ->
+  | [BFcast], { v = CCast (c, Glob_term.CastConv t) } ->
     [Bcast t], c
   | BFrec (has_str, has_cast) :: h, 
     { v = CFix ( _, [_, (Some locn, CStructRec), bl, t, c]) } ->
@@ -1093,7 +1093,7 @@ let wit_ssrfwdfmt = add_genarg "ssrfwdfmt" pr_fwdfmt
 
 let mkFwdVal fk c = ((fk, []), c)
 let mkssrFwdVal fk c = ((fk, []), (c,None))
-let dC t = CastConv t
+let dC t = Glob_term.CastConv t
 
 let same_ist { interp_env = x } { interp_env = y } =
   match x,y with
@@ -1210,8 +1210,8 @@ let push_binders c2 bs =
   | [] -> c
   | _ -> anomaly "binder not a lambda nor a let in" in
   match c2 with
-  | { loc; v = CCast (ct, CastConv cty) } ->
-      CAst.make ?loc @@ (CCast (loop false ct bs, CastConv (loop true cty bs)))
+  | { loc; v = CCast (ct, Glob_term.CastConv cty) } ->
+      CAst.make ?loc @@ (CCast (loop false ct bs, Glob_term.CastConv (loop true cty bs)))
   | ct -> loop false ct bs
 
 let rec fix_binders = let open CAst in function
diff --git a/plugins/ssr/ssrtacticals.ml b/plugins/ssr/ssrtacticals.ml
index 372ae86bd..83581f341 100644
--- a/plugins/ssr/ssrtacticals.ml
+++ b/plugins/ssr/ssrtacticals.ml
@@ -14,7 +14,6 @@ open Names
 open Constr
 open Termops
 open Tacmach
-open Misctypes
 open Locusops
 
 open Ssrast
@@ -25,7 +24,7 @@ module NamedDecl = Context.Named.Declaration
 
 (** Tacticals (+, -, *, done, by, do, =>, first, and last). *)
 
-let get_index = function ArgArg i -> i | _ ->
+let get_index = function Locus.ArgArg i -> i | _ ->
   anomaly "Uninterpreted index"
 (* Toplevel constr must be globalized twice ! *)
 
diff --git a/plugins/ssr/ssrtacticals.mli b/plugins/ssr/ssrtacticals.mli
index a5636ad0f..684e00235 100644
--- a/plugins/ssr/ssrtacticals.mli
+++ b/plugins/ssr/ssrtacticals.mli
@@ -17,7 +17,7 @@ val tclSEQAT :
   Tacinterp.interp_sign ->
   Tacinterp.Value.t ->
   Ssrast.ssrdir ->
-  int Misctypes.or_var *
+  int Locus.or_var *
     (('a * Tacinterp.Value.t option list) *
        Tacinterp.Value.t option) ->
   Tacmach.tactic
@@ -37,7 +37,7 @@ val hinttac :
 
 val ssrdotac :
   Tacinterp.interp_sign ->
-  ((int Misctypes.or_var * Ssrast.ssrmmod) *
+  ((int Locus.or_var * Ssrast.ssrmmod) *
      (bool * Tacinterp.Value.t option list)) *
     ((Ssrast.ssrhyps *
         ((Ssrast.ssrhyp_or_id * string) *
diff --git a/plugins/ssr/ssrvernac.ml4 b/plugins/ssr/ssrvernac.ml4
index 750461a1b..939e97866 100644
--- a/plugins/ssr/ssrvernac.ml4
+++ b/plugins/ssr/ssrvernac.ml4
@@ -27,7 +27,6 @@ open Glob_term
 open Globnames
 open Stdarg
 open Genarg
-open Misctypes
 open Decl_kinds
 open Libnames
 open Pp
diff --git a/plugins/ssr/ssrview.ml b/plugins/ssr/ssrview.ml
index 29a936381..faebe3179 100644
--- a/plugins/ssr/ssrview.ml
+++ b/plugins/ssr/ssrview.ml
@@ -157,7 +157,7 @@ let tclINJ_CONSTR_IST ist p =
 
 let mkGHole =
   DAst.make
-    (Glob_term.GHole(Evar_kinds.InternalHole, Misctypes.IntroAnonymous, None))
+    (Glob_term.GHole(Evar_kinds.InternalHole, Namegen.IntroAnonymous, None))
 let rec mkGHoles n = if n > 0 then mkGHole :: mkGHoles (n - 1) else []
 let mkGApp f args =
   if args = [] then f
diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4
index b1c5e131f..69d944fa1 100644
--- a/plugins/ssrmatching/ssrmatching.ml4
+++ b/plugins/ssrmatching/ssrmatching.ml4
@@ -40,7 +40,7 @@ open Pretyping
 open Ppconstr
 open Printer
 open Globnames
-open Misctypes
+open Namegen
 open Decl_kinds
 open Evar_kinds
 open Constrexpr
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 1edce17bd..aa1c23f52 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -2103,7 +2103,7 @@ let mk_JMeq_refl evdref typ x =
 
 let hole na = DAst.make @@
   GHole (Evar_kinds.QuestionMark (Evar_kinds.Define false,na),
-         Misctypes.IntroAnonymous, None)
+         IntroAnonymous, None)
 
 let constr_of_pat env evdref arsign pat avoid =
   let rec typ env (ty, realargs) pat avoid =
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index e6cfe1f76..df89d9eac 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -27,7 +27,6 @@ open Libnames
 open Globnames
 open Nametab
 open Mod_subst
-open Misctypes
 open Decl_kinds
 open Context.Named.Declaration
 open Ltac_pretype
@@ -1027,7 +1026,7 @@ let rec subst_glob_constr subst = DAst.map (function
 
   | GCast (r1,k) as raw ->
       let r1' = subst_glob_constr subst r1 in
-      let k' = Miscops.smartmap_cast_type (subst_glob_constr subst) k in
+      let k' = smartmap_cast_type (subst_glob_constr subst) k in
       if r1' == r1 && k' == k then raw else GCast (r1',k')
 
   | GProj (p,c) as raw ->
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index 63618c918..71a457280 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -11,10 +11,8 @@
 open Util
 open CAst
 open Names
-open Constr
 open Nameops
 open Globnames
-open Misctypes
 open Glob_term
 open Evar_kinds
 open Ltac_pretype
@@ -48,12 +46,20 @@ let map_glob_decl_left_to_right f (na,k,obd,ty) =
   let comp2 = f ty in
   (na,k,comp1,comp2)
 
+
+let glob_sort_eq g1 g2 = let open Glob_term in match g1, g2 with
+| GProp, GProp -> true
+| GSet, GSet -> true
+| GType l1, GType l2 ->
+   List.equal (Option.equal (fun (x,m) (y,n) -> Libnames.eq_reference x y && Int.equal m n)) l1 l2
+| _ -> false
+
 let binding_kind_eq bk1 bk2 = match bk1, bk2 with
   | Decl_kinds.Explicit, Decl_kinds.Explicit -> true
   | Decl_kinds.Implicit, Decl_kinds.Implicit -> true
   | (Decl_kinds.Explicit | Decl_kinds.Implicit), _ -> false
 
-let case_style_eq s1 s2 = match s1, s2 with
+let case_style_eq s1 s2 = let open Constr in match s1, s2 with
   | LetStyle, LetStyle -> true
   | IfStyle, IfStyle -> true
   | LetPatternStyle, LetPatternStyle -> true
@@ -141,10 +147,10 @@ let mk_glob_constr_eq f c1 c2 = match DAst.get c1, DAst.get c2 with
     fix_kind_eq f kn1 kn2 && Array.equal Id.equal id1 id2 &&
     Array.equal (fun l1 l2 -> List.equal (glob_decl_eq f) l1 l2) decl1 decl2 &&
     Array.equal f c1 c2 && Array.equal f t1 t2
-  | GSort s1, GSort s2 -> Miscops.glob_sort_eq s1 s2
+  | GSort s1, GSort s2 -> glob_sort_eq s1 s2
   | GHole (kn1, nam1, gn1), GHole (kn2, nam2, gn2) ->
     Option.equal (==) gn1 gn2 (** Only thing sensible *) &&
-    Miscops.intro_pattern_naming_eq nam1 nam2
+    Namegen.intro_pattern_naming_eq nam1 nam2
   | GCast (c1, t1), GCast (c2, t2) ->
     f c1 c2 && cast_type_eq f t1 t2
   | GProj (p1, t1), GProj (p2, t2) ->
@@ -154,6 +160,21 @@ let mk_glob_constr_eq f c1 c2 = match DAst.get c1, DAst.get c2 with
 
 let rec glob_constr_eq c = mk_glob_constr_eq glob_constr_eq c
 
+(** Mapping [cast_type] *)
+
+let map_cast_type f = function
+  | CastConv a -> CastConv (f a)
+  | CastVM a -> CastVM (f a)
+  | CastCoerce -> CastCoerce
+  | CastNative a -> CastNative (f a)
+
+let smartmap_cast_type f c =
+  match c with
+    | CastConv a -> let a' = f a in if a' == a then c else CastConv a'
+    | CastVM a -> let a' = f a in if a' == a then c else CastVM a'
+    | CastCoerce -> CastCoerce
+    | CastNative a -> let a' = f a in if a' == a then c else CastNative a'
+
 let map_glob_constr_left_to_right f = DAst.map (function
   | GApp (g,args) ->
       let comp1 = f g in
@@ -194,7 +215,7 @@ let map_glob_constr_left_to_right f = DAst.map (function
       GRec (fk,idl,comp1,comp2,comp3)
   | GCast (c,k) ->
       let comp1 = f c in
-      let comp2 = Miscops.map_cast_type f k in
+      let comp2 = map_cast_type f k in
       GCast (comp1,comp2)
   | GProj (p,c) ->
     GProj (p, f c)
@@ -539,7 +560,7 @@ let rec glob_constr_of_cases_pattern_aux isclosed x = DAst.map_with_loc (fun ?lo
   | PatVar (Name id) when not isclosed ->
       GVar id
   | PatVar Anonymous when not isclosed ->
-      GHole (Evar_kinds.QuestionMark (Define false,Anonymous),Misctypes.IntroAnonymous,None)
+      GHole (Evar_kinds.QuestionMark (Define false,Anonymous),Namegen.IntroAnonymous,None)
   | _ -> raise Not_found
   ) x
 
diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli
index 124440f5d..c967f4e88 100644
--- a/pretyping/glob_ops.mli
+++ b/pretyping/glob_ops.mli
@@ -13,6 +13,8 @@ open Glob_term
 
 (** Equalities *)
 
+val glob_sort_eq : Glob_term.glob_sort -> Glob_term.glob_sort -> bool
+
 val cases_pattern_eq : 'a cases_pattern_g -> 'a cases_pattern_g -> bool
 
 val alias_of_pat : 'a cases_pattern_g -> Name.t
@@ -20,10 +22,15 @@ val alias_of_pat : 'a cases_pattern_g -> Name.t
 val set_pat_alias : Id.t -> 'a cases_pattern_g -> 'a cases_pattern_g
 
 val cast_type_eq : ('a -> 'a -> bool) ->
-  'a Misctypes.cast_type -> 'a Misctypes.cast_type -> bool
+  'a cast_type -> 'a cast_type -> bool
 
 val glob_constr_eq : 'a glob_constr_g -> 'a glob_constr_g -> bool
 
+(** Mapping [cast_type] *)
+
+val map_cast_type : ('a -> 'b) -> 'a cast_type -> 'b cast_type
+val smartmap_cast_type : ('a -> 'a) -> 'a cast_type -> 'a cast_type
+
 (** Operations on [glob_constr] *)
 
 val cases_pattern_loc : 'a cases_pattern_g -> Loc.t option
diff --git a/pretyping/glob_term.ml b/pretyping/glob_term.ml
index 6ecb479e6..54fa5328f 100644
--- a/pretyping/glob_term.ml
+++ b/pretyping/glob_term.ml
@@ -18,7 +18,6 @@
 
 open Names
 open Decl_kinds
-open Misctypes
 
 type existential_name = Id.t
 
@@ -41,6 +40,14 @@ type glob_constraint = glob_level * Univ.constraint_type * glob_level
 type sort_info = (Libnames.reference * int) option list
 type glob_sort = sort_info glob_sort_gen
 
+(** Casts *)
+
+type 'a cast_type =
+  | CastConv of 'a
+  | CastVM of 'a
+  | CastCoerce (** Cast to a base type (eg, an underlying inductive type) *)
+  | CastNative of 'a
+
 (**  The kind of patterns that occurs in "match ... with ... end"
 
      locs here refers to the ident's location, not whole pat *)
@@ -73,7 +80,7 @@ type 'a glob_constr_r =
   | GRec  of 'a fix_kind_g * Id.t array * 'a glob_decl_g list array *
              'a glob_constr_g array * 'a glob_constr_g array
   | GSort of glob_sort
-  | GHole of Evar_kinds.t * intro_pattern_naming_expr * Genarg.glob_generic_argument option
+  | GHole of Evar_kinds.t * Namegen.intro_pattern_naming_expr * Genarg.glob_generic_argument option
   | GCast of 'a glob_constr_g * 'a glob_constr_g cast_type
   | GProj of Projection.t * 'a glob_constr_g
 and 'a glob_constr_g = ('a glob_constr_r, 'a) DAst.t
diff --git a/pretyping/locus.ml b/pretyping/locus.ml
index 95a2e495b..37dd120c1 100644
--- a/pretyping/locus.ml
+++ b/pretyping/locus.ml
@@ -9,10 +9,13 @@
 (************************************************************************)
 
 open Names
-open Misctypes
 
 (** Locus : positions in hypotheses and goals *)
 
+type 'a or_var =
+  | ArgArg of 'a
+  | ArgVar of lident
+
 (** {6 Occurrences} *)
 
 type 'a occurrences_gen =
diff --git a/pretyping/locusops.ml b/pretyping/locusops.ml
index 1664e68f2..6b6a3f8a9 100644
--- a/pretyping/locusops.ml
+++ b/pretyping/locusops.ml
@@ -86,8 +86,8 @@ let concrete_clause_of enum_hyps cl =
 (** Miscellaneous functions *)
 
 let out_arg = function
-  | Misctypes.ArgVar _ -> CErrors.anomaly (Pp.str "Unevaluated or_var variable.")
-  | Misctypes.ArgArg x -> x
+  | ArgVar _ -> CErrors.anomaly (Pp.str "Unevaluated or_var variable.")
+  | ArgArg x -> x
 
 let occurrences_of_hyp id cls =
   let rec hyp_occ = function
diff --git a/pretyping/miscops.ml b/pretyping/miscops.ml
deleted file mode 100644
index 1697e54ab..000000000
--- a/pretyping/miscops.ml
+++ /dev/null
@@ -1,55 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
-(* <O___,, *       (see CREDITS file for the list of authors)           *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-open Util
-open Misctypes
-
-(** Mapping [cast_type] *)
-
-let map_cast_type f = function
-  | CastConv a -> CastConv (f a)
-  | CastVM a -> CastVM (f a)
-  | CastCoerce -> CastCoerce
-  | CastNative a -> CastNative (f a)
-
-let smartmap_cast_type f c =
-  match c with
-    | CastConv a -> let a' = f a in if a' == a then c else CastConv a'
-    | CastVM a -> let a' = f a in if a' == a then c else CastVM a'
-    | CastCoerce -> CastCoerce
-    | CastNative a -> let a' = f a in if a' == a then c else CastNative a'
-
-(** Equalities on [glob_sort] *)
-
-let glob_sort_eq g1 g2 = let open Glob_term in match g1, g2 with
-| GProp, GProp -> true
-| GSet, GSet -> true
-| GType l1, GType l2 ->
-   List.equal (Option.equal (fun (x,m) (y,n) -> Libnames.eq_reference x y && Int.equal m n)) l1 l2
-| _ -> false
-
-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
-
-(** Mapping bindings *)
-
-let map_explicit_bindings f l =
-  let map = CAst.map (fun (hyp, x) -> (hyp, f x)) in
-  List.map map l
-
-let map_bindings f = function
-| ImplicitBindings l -> ImplicitBindings (List.map f l)
-| ExplicitBindings expl -> ExplicitBindings (map_explicit_bindings f expl)
-| NoBindings -> NoBindings
-
-let map_with_bindings f (x, bl) = (f x, map_bindings f bl)
diff --git a/pretyping/miscops.mli b/pretyping/miscops.mli
deleted file mode 100644
index 6a84fb9eb..000000000
--- a/pretyping/miscops.mli
+++ /dev/null
@@ -1,30 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
-(* <O___,, *       (see CREDITS file for the list of authors)           *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-open Misctypes
-
-(** Mapping [cast_type] *)
-
-val map_cast_type : ('a -> 'b) -> 'a cast_type -> 'b cast_type
-val smartmap_cast_type : ('a -> 'a) -> 'a cast_type -> 'a cast_type
-
-(** Equalities on [glob_sort] *)
-
-val glob_sort_eq : Glob_term.glob_sort -> Glob_term.glob_sort -> bool
-
-(** Equalities on [intro_pattern_naming] *)
-
-val intro_pattern_naming_eq :
-  intro_pattern_naming_expr -> intro_pattern_naming_expr -> bool
-
-(** Mapping bindings *)
-
-val map_bindings : ('a -> 'b) -> 'a bindings -> 'b bindings
-val map_with_bindings : ('a -> 'b) -> 'a with_bindings -> 'b with_bindings
diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml
index 996a2dc36..be7ebe49c 100644
--- a/pretyping/pattern.ml
+++ b/pretyping/pattern.ml
@@ -9,10 +9,12 @@
 (************************************************************************)
 
 open Names
-open Misctypes
 
 (** {5 Patterns} *)
 
+(** Cases pattern variables *)
+type patvar = Id.t
+
 type case_info_pattern =
     { cip_style : Constr.case_style;
       cip_ind : inductive option;
@@ -22,7 +24,7 @@ type case_info_pattern =
 type constr_pattern =
   | PRef of GlobRef.t
   | PVar of Id.t
-  | PEvar of existential_key * constr_pattern array
+  | PEvar of Evar.t * constr_pattern array
   | PRel of int
   | PApp of constr_pattern * constr_pattern array
   | PSoApp of patvar * constr_pattern list
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index 9342b4cc7..622a8e982 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -18,7 +18,6 @@ open Constr
 open Glob_term
 open Pp
 open Mod_subst
-open Misctypes
 open Decl_kinds
 open Pattern
 open Environ
@@ -47,7 +46,7 @@ let rec constr_pattern_eq p1 p2 = match p1, p2 with
 | PLetIn (v1, b1, t1, c1), PLetIn (v2, b2, t2, c2) ->
   Name.equal v1 v2 && constr_pattern_eq b1 b2 &&
   Option.equal constr_pattern_eq t1 t2 && constr_pattern_eq c1 c2
-| PSort s1, PSort s2 -> Miscops.glob_sort_eq s1 s2
+| PSort s1, PSort s2 -> Glob_ops.glob_sort_eq s1 s2
 | PMeta m1, PMeta m2 -> Option.equal Id.equal m1 m2
 | PIf (t1, l1, r1), PIf (t2, l2, r2) ->
   constr_pattern_eq t1 t2 && constr_pattern_eq l1 l2 && constr_pattern_eq r1 r2
@@ -418,7 +417,7 @@ let rec pat_of_raw metas vars = DAst.with_loc_val (fun ?loc -> function
            pat_of_raw metas vars b1,pat_of_raw metas vars b2)
   | GLetTuple (nal,(_,None),b,c) ->
       let mkGLambda na c = DAst.make ?loc @@
-	GLambda (na,Explicit, DAst.make @@ GHole (Evar_kinds.InternalHole, IntroAnonymous, None),c) in
+        GLambda (na,Explicit, DAst.make @@ GHole (Evar_kinds.InternalHole, Namegen.IntroAnonymous, None),c) in
       let c = List.fold_right mkGLambda nal c in
       let cip =
 	{ cip_style = LetStyle;
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/pretyping.ml b/pretyping/pretyping.ml
index b2507b5f2..9e024b1c2 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -45,7 +45,6 @@ open Pretype_errors
 open Glob_term
 open Glob_ops
 open Evarconv
-open Misctypes
 open Ltac_pretype
 
 module NamedDecl = Context.Named.Declaration
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.ml b/printing/ppconstr.ml
index e877b3c63..605781993 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -15,15 +15,15 @@ open Pp
 open CAst
 open Names
 open Nameops
-open Constr
 open Libnames
 open Pputils
 open Ppextend
-open Notation_gram
+open Glob_term
 open Constrexpr
 open Constrexpr_ops
+open Notation_gram
 open Decl_kinds
-open Misctypes
+open Namegen
 (*i*)
 
 module Tag =
@@ -228,7 +228,7 @@ let tag_var = tag Tag.variable
         str "(" ++ pr_id id ++ str ":=" ++ pr ltop a ++ str ")"
 
   let pr_opt_type_spc pr = function
-    | { CAst.v = CHole (_,Misctypes.IntroAnonymous,_) } -> mt ()
+    | { CAst.v = CHole (_,IntroAnonymous,_) } -> mt ()
     | t ->  str " :" ++ pr_sep_com (fun()->brk(1,2)) (pr ltop) t
 
   let pr_lident {loc; v=id} =
@@ -242,8 +242,8 @@ let tag_var = tag Tag.variable
     | x -> pr_ast Name.print x
 
   let pr_or_var pr = function
-    | ArgArg x -> pr x
-    | ArgVar id -> pr_lident id
+    | Locus.ArgArg x -> pr x
+    | Locus.ArgVar id -> pr_lident id
 
   let pr_prim_token = function
     | Numeral (n,s) -> str (if s then n else "-"^n)
@@ -363,7 +363,7 @@ let tag_var = tag Tag.variable
         end
       | Default b ->
         match t with
-          | { CAst.v = CHole (_,Misctypes.IntroAnonymous,_) } ->
+          | { CAst.v = CHole (_,IntroAnonymous,_) } ->
             let s = prlist_with_sep spc pr_lname nal in
             hov 1 (surround_implicit b s)
           | _ ->
@@ -457,7 +457,7 @@ let tag_var = tag Tag.variable
 
   let pr_case_type pr po =
     match po with
-      | None | Some { CAst.v = CHole (_,Misctypes.IntroAnonymous,_) } -> mt()
+      | None | Some { CAst.v = CHole (_,IntroAnonymous,_) } -> mt()
       | Some p ->
         spc() ++ hov 2 (keyword "return" ++ pr_sep_com spc (pr lsimpleconstr) p)
 
@@ -592,7 +592,7 @@ let tag_var = tag Tag.variable
           hv 0 (str"{|" ++ pr_record_body_gen (pr spc) l ++ str" |}"),
           latom
         )
-      | CCases (LetPatternStyle,rtntypopt,[c,as_clause,in_clause],[{v=([[p]],b)}]) ->
+      | CCases (Constr.LetPatternStyle,rtntypopt,[c,as_clause,in_clause],[{v=([[p]],b)}]) ->
         return (
           hv 0 (
             keyword "let" ++ spc () ++ str"'" ++
@@ -643,9 +643,9 @@ let tag_var = tag Tag.variable
         lif
         )
 
-      | CHole (_,Misctypes.IntroIdentifier id,_) ->
+      | CHole (_,IntroIdentifier id,_) ->
         return (str "?[" ++ pr_id id ++ str "]", latom)
-      | CHole (_,Misctypes.IntroFresh id,_) ->
+      | CHole (_,IntroFresh id,_) ->
         return (str "?[?" ++ pr_id id ++ str "]", latom)
       | CHole (_,_,_) ->
         return (str "_", latom)
diff --git a/printing/ppconstr.mli b/printing/ppconstr.mli
index 05f48ec79..ce37c3614 100644
--- a/printing/ppconstr.mli
+++ b/printing/ppconstr.mli
@@ -15,14 +15,13 @@
 open Libnames
 open Constrexpr
 open Names
-open Misctypes
 open Notation_gram
 
 val prec_less : precedence -> tolerability -> bool
 
 val pr_tight_coma : unit -> Pp.t
 
-val pr_or_var : ('a -> Pp.t) -> 'a or_var -> Pp.t
+val pr_or_var : ('a -> Pp.t) -> 'a Locus.or_var -> Pp.t
 
 val pr_lident : lident -> Pp.t
 val pr_lname : lname -> Pp.t
@@ -39,7 +38,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/printing/pputils.ml b/printing/pputils.ml
index c14aa318e..c6b8d5022 100644
--- a/printing/pputils.ml
+++ b/printing/pputils.ml
@@ -11,7 +11,6 @@
 open Util
 open Pp
 open Genarg
-open Misctypes
 open Locus
 open Genredexpr
 
@@ -122,7 +121,7 @@ let pr_red_expr (pr_constr,pr_lconstr,pr_ref,pr_pattern) keyword = function
 let pr_red_expr_env env sigma (pr_constr,pr_lconstr,pr_ref,pr_pattern) =
   pr_red_expr (pr_constr env sigma, pr_lconstr env sigma, pr_ref, pr_pattern env sigma)
 
-let pr_or_by_notation f = function
+let pr_or_by_notation f = let open Constrexpr in function
   | {CAst.loc; v=AN v} -> f v
   | {CAst.loc; v=ByNotation (s,sc)} -> qs s ++ pr_opt (fun sc -> str "%" ++ str sc) sc
 
diff --git a/printing/pputils.mli b/printing/pputils.mli
index 6039168f8..5b1969e23 100644
--- a/printing/pputils.mli
+++ b/printing/pputils.mli
@@ -9,7 +9,6 @@
 (************************************************************************)
 
 open Genarg
-open Misctypes
 open Locus
 open Genredexpr
 
@@ -18,7 +17,7 @@ val pr_ast : ('a -> Pp.t) -> 'a CAst.t -> Pp.t
 (** Prints an object surrounded by its commented location *)
 
 val pr_or_var : ('a -> Pp.t) -> 'a or_var -> Pp.t
-val pr_or_by_notation : ('a -> Pp.t) -> 'a or_by_notation -> Pp.t
+val pr_or_by_notation : ('a -> Pp.t) -> 'a Constrexpr.or_by_notation -> Pp.t
 val pr_with_occurrences :
   ('a -> Pp.t) -> (string -> Pp.t) -> 'a with_occurrences -> Pp.t
 
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index 895181bc5..fe6cf73c7 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -26,7 +26,6 @@ open Libobject
 open Libnames
 open Globnames
 open Recordops
-open Misctypes
 open Printer
 open Printmod
 open Context.Rel.Declaration
@@ -843,12 +842,12 @@ let print_any_name env sigma na udecl =
 
 let print_name env sigma na udecl =
   match na with
-  | {loc; v=ByNotation (ntn,sc)} ->
+  | {loc; v=Constrexpr.ByNotation (ntn,sc)} ->
       print_any_name env sigma
         (Term (Notation.interp_notation_as_global_reference ?loc (fun _ -> true)
                ntn sc))
         udecl
-  | {loc; v=AN ref} ->
+  | {loc; v=Constrexpr.AN ref} ->
       print_any_name env sigma (locate_any_name ref) udecl
 
 let print_opaque_name env sigma qid =
@@ -896,11 +895,11 @@ let print_about_any ?loc env sigma k udecl =
 
 let print_about env sigma na udecl =
   match na with
-  | {loc;v=ByNotation (ntn,sc)} ->
+  | {loc;v=Constrexpr.ByNotation (ntn,sc)} ->
       print_about_any ?loc env sigma
         (Term (Notation.interp_notation_as_global_reference ?loc (fun _ -> true)
                ntn sc)) udecl
-  | {loc;v=AN ref} ->
+  | {loc;v=Constrexpr.AN ref} ->
       print_about_any ?loc env sigma (locate_any_name ref) udecl
 
 (* for debug *)
diff --git a/printing/prettyp.mli b/printing/prettyp.mli
index 50042d6c5..0375cfc92 100644
--- a/printing/prettyp.mli
+++ b/printing/prettyp.mli
@@ -12,7 +12,6 @@ open Names
 open Environ
 open Reductionops
 open Libnames
-open Misctypes
 open Evd
 
 (** A Pretty-Printer for the Calculus of Inductive Constructions. *)
@@ -33,12 +32,12 @@ val print_eval :
   reduction_function -> env -> Evd.evar_map ->
     Constrexpr.constr_expr -> EConstr.unsafe_judgment -> Pp.t
 
-val print_name : env -> Evd.evar_map -> reference or_by_notation ->
+val print_name : env -> Evd.evar_map -> reference Constrexpr.or_by_notation ->
   UnivNames.univ_name_list option -> Pp.t
 val print_opaque_name : env -> Evd.evar_map -> reference -> Pp.t
-val print_about : env -> Evd.evar_map -> reference or_by_notation ->
+val print_about : env -> Evd.evar_map -> reference Constrexpr.or_by_notation ->
   UnivNames.univ_name_list option -> Pp.t
-val print_impargs : reference or_by_notation -> Pp.t
+val print_impargs : reference Constrexpr.or_by_notation -> Pp.t
 
 (** Pretty-printing functions for classes and coercions *)
 val print_graph : env -> evar_map -> Pp.t
diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 450fcddfd..79b7e1599 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -26,7 +26,7 @@ open Tacred
 open Pretype_errors
 open Evarutil
 open Unification
-open Misctypes
+open Tactypes
 
 (******************************************************************)
 (* Clausal environments *)
diff --git a/proofs/clenv.mli b/proofs/clenv.mli
index b85c4fc51..f9506290a 100644
--- a/proofs/clenv.mli
+++ b/proofs/clenv.mli
@@ -18,7 +18,7 @@ open Environ
 open Evd
 open EConstr
 open Unification
-open Misctypes
+open Tactypes
 
 (** {6 The Type of Constructions clausale environments.} *)
 
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index 38ed63c23..544175c6d 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -54,7 +54,7 @@ let clenv_cast_meta clenv =
 let clenv_value_cast_meta clenv =
     clenv_cast_meta clenv (clenv_value clenv)
 
-let clenv_pose_dependent_evars with_evars clenv =
+let clenv_pose_dependent_evars ?(with_evars=false) clenv =
   let dep_mvs = clenv_dependent clenv in
   let env, sigma = clenv.env, clenv.evd in
   if not (List.is_empty dep_mvs) && not with_evars then
@@ -75,12 +75,12 @@ let check_tc evd =
   let has_typeclass = Evar.Map.exists check (Evd.undefined_map evd) in
   (has_typeclass, !has_resolvable)
 
-let clenv_refine with_evars ?(with_classes=true) clenv =
+let clenv_refine ?(with_evars=false) ?(with_classes=true) clenv =
   (** ppedrot: a Goal.enter here breaks things, because the tactic below may
       solve goals by side effects, while the compatibility layer keeps those
       useless goals. That deserves a FIXME. *)
   Proofview.V82.tactic begin fun gl ->
-  let clenv = clenv_pose_dependent_evars with_evars clenv in
+  let clenv = clenv_pose_dependent_evars ~with_evars clenv in
   let evd' =
     if with_classes then
       let (has_typeclass, has_resolvable) = check_tc clenv.evd in
@@ -105,10 +105,10 @@ open Unification
 
 let dft = default_unify_flags
 
-let res_pf ?(with_evars=false) ?(with_classes=true) ?(flags=dft ()) clenv =
+let res_pf ?with_evars ?(with_classes=true) ?(flags=dft ()) clenv =
   Proofview.Goal.enter begin fun gl ->
     let clenv = clenv_unique_resolver ~flags clenv gl in
-    clenv_refine with_evars ~with_classes clenv
+    clenv_refine ?with_evars ~with_classes clenv
   end
 
 (* [unifyTerms] et [unify] ne semble pas gérer les Meta, en
diff --git a/proofs/clenvtac.mli b/proofs/clenvtac.mli
index 7c1e300b8..d17847842 100644
--- a/proofs/clenvtac.mli
+++ b/proofs/clenvtac.mli
@@ -13,12 +13,11 @@
 open Clenv
 open EConstr
 open Unification
-open Misctypes
 
 (** Tactics *)
 val unify : ?flags:unify_flags -> constr -> unit Proofview.tactic
-val clenv_refine : evars_flag -> ?with_classes:bool -> clausenv -> unit Proofview.tactic
-val res_pf : ?with_evars:evars_flag -> ?with_classes:bool -> ?flags:unify_flags -> clausenv -> unit Proofview.tactic
+val clenv_refine : ?with_evars:bool -> ?with_classes:bool -> clausenv -> unit Proofview.tactic
+val res_pf : ?with_evars:bool -> ?with_classes:bool -> ?flags:unify_flags -> clausenv -> unit Proofview.tactic
 
-val clenv_pose_dependent_evars : evars_flag -> clausenv -> clausenv
+val clenv_pose_dependent_evars : ?with_evars:bool -> clausenv -> clausenv
 val clenv_value_cast_meta : clausenv -> constr
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 95c30d815..e8ca71993 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -23,7 +23,6 @@ open Typing
 open Proof_type
 open Type_errors
 open Retyping
-open Misctypes
 
 module NamedDecl = Context.Named.Declaration
 
@@ -185,6 +184,22 @@ let check_decl_position env sigma sign d =
  * on the right side [right] if [toleft=false].
  * If [with_dep] then dependent hypotheses are moved accordingly. *)
 
+(** Move destination for hypothesis *)
+
+type 'id move_location =
+  | MoveAfter of 'id
+  | MoveBefore of 'id
+  | MoveFirst
+  | MoveLast (** can be seen as "no move" when doing intro *)
+
+(** Printing of [move_location] *)
+
+let pr_move_location pr_id = function
+  | MoveAfter id -> brk(1,1) ++ str "after " ++ pr_id id
+  | MoveBefore id -> brk(1,1) ++ str "before " ++ pr_id id
+  | MoveFirst -> str " at top"
+  | MoveLast -> str " at bottom"
+
 let move_location_eq m1 m2 = match m1, m2 with
 | MoveAfter id1, MoveAfter id2 -> Id.equal id1 id2
 | MoveBefore id1, MoveBefore id2 -> Id.equal id1 id2
@@ -236,7 +251,7 @@ let move_hyp sigma toleft (left,declfrom,right) hto =
 	      (first, d::middle)
             else
 	      user_err ~hdr:"move_hyp" (str "Cannot move " ++ Id.print (NamedDecl.get_id declfrom) ++
-	        Miscprint.pr_move_location Id.print hto ++
+                pr_move_location Id.print hto ++
 	        str (if toleft then ": it occurs in the type of " else ": it depends on ")
 	        ++ Id.print hyp ++ str ".")
           else
diff --git a/proofs/logic.mli b/proofs/logic.mli
index dc471bb5f..9db54732b 100644
--- a/proofs/logic.mli
+++ b/proofs/logic.mli
@@ -58,12 +58,23 @@ val error_no_such_hypothesis : Environ.env -> evar_map -> Id.t -> 'a
 
 val catchable_exception : exn -> bool
 
+(** Move destination for hypothesis *)
+
+type 'id move_location =
+  | MoveAfter of 'id
+  | MoveBefore of 'id
+  | MoveFirst
+  | MoveLast (** can be seen as "no move" when doing intro *)
+
+val pr_move_location :
+  ('a -> Pp.t) -> 'a move_location -> Pp.t
+
 val convert_hyp : bool -> Environ.named_context_val -> evar_map ->
   EConstr.named_declaration -> Environ.named_context_val
 
-val move_hyp_in_named_context : Environ.env -> Evd.evar_map -> Id.t -> Id.t Misctypes.move_location ->
+val move_hyp_in_named_context : Environ.env -> Evd.evar_map -> Id.t -> Id.t move_location ->
   Environ.named_context_val -> Environ.named_context_val
 
 val insert_decl_in_named_context : Evd.evar_map ->
-  EConstr.named_declaration -> Id.t Misctypes.move_location ->
+  EConstr.named_declaration -> Id.t move_location ->
   Environ.named_context_val -> Environ.named_context_val
diff --git a/proofs/miscprint.ml b/proofs/miscprint.ml
index 1a63ff673..ec17b8076 100644
--- a/proofs/miscprint.ml
+++ b/proofs/miscprint.ml
@@ -10,7 +10,7 @@
 
 open Pp
 open Names
-open Misctypes
+open Tactypes
 
 (** Printing of [intro_pattern] *)
 
@@ -20,7 +20,7 @@ let rec pr_intro_pattern prc {CAst.v=pat} = match pat with
   | IntroNaming p -> pr_intro_pattern_naming p
   | IntroAction p -> pr_intro_pattern_action prc p
 
-and pr_intro_pattern_naming = function
+and pr_intro_pattern_naming = let open Namegen in function
   | IntroIdentifier id -> Id.print id
   | IntroFresh id -> str "?" ++ Id.print id
   | IntroAnonymous -> str "?"
@@ -43,14 +43,6 @@ and pr_or_and_intro_pattern prc = function
       hv 0 (prlist_with_sep pr_bar (prlist_with_sep spc (pr_intro_pattern prc)) pll)
       ++ str "]"
 
-(** Printing of [move_location] *)
-
-let pr_move_location pr_id = function
-  | MoveAfter id -> brk(1,1) ++ str "after " ++ pr_id id
-  | MoveBefore id -> brk(1,1) ++ str "before " ++ pr_id id
-  | MoveFirst -> str " at top"
-  | MoveLast -> str " at bottom"
-
 (** Printing of bindings *)
 let pr_binding prc = let open CAst in function
   | {loc;v=(NamedHyp id, c)} -> hov 1 (Names.Id.print id ++ str " := " ++ cut () ++ prc c)
diff --git a/proofs/miscprint.mli b/proofs/miscprint.mli
index 79790a277..f4e2e683d 100644
--- a/proofs/miscprint.mli
+++ b/proofs/miscprint.mli
@@ -8,7 +8,7 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-open Misctypes
+open Tactypes
 
 (** Printing of [intro_pattern] *)
 
@@ -18,13 +18,10 @@ val pr_intro_pattern :
 val pr_or_and_intro_pattern :
   ('a -> Pp.t) -> 'a or_and_intro_pattern_expr -> Pp.t
 
-val pr_intro_pattern_naming : intro_pattern_naming_expr -> Pp.t
+val pr_intro_pattern_naming : Namegen.intro_pattern_naming_expr -> Pp.t
 
 (** Printing of [move_location] *)
 
-val pr_move_location :
-  ('a -> Pp.t) -> 'a move_location -> Pp.t
-
 val pr_bindings :
   ('a -> Pp.t) ->
   ('a -> Pp.t) -> 'a bindings -> 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/proofs/redexpr.ml b/proofs/redexpr.ml
index 03ebc3275..629b77be2 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -23,7 +23,6 @@ open Tacred
 open CClosure
 open RedFlags
 open Libobject
-open Misctypes
 
 (* call by value normalisation function using the virtual machine *)
 let cbv_vm env sigma c =
@@ -200,8 +199,8 @@ let decl_red_expr s e =
   end
 
 let out_arg = function
-  | ArgVar _ -> anomaly (Pp.str "Unevaluated or_var variable.")
-  | ArgArg x -> x
+  | Locus.ArgVar _ -> anomaly (Pp.str "Unevaluated or_var variable.")
+  | Locus.ArgArg x -> x
 
 let out_with_occurrences (occs,c) =
   (Locusops.occurrences_map (List.map out_arg) occs, c)
diff --git a/interp/tactypes.ml b/proofs/tactypes.ml
index 83e42be89..86a7e9c52 100644
--- a/interp/tactypes.ml
+++ b/proofs/tactypes.ml
@@ -13,15 +13,35 @@
     meant to stay. *)
 
 open Names
-open Constrexpr
-open Pattern
-open Misctypes
 
-(** In globalize tactics, we need to keep the initial [constr_expr] to recompute
-   in the environment by the effective calls to Intro, Inversion, etc 
-   The [constr_expr] field is [None] in TacDef though *)
-type glob_constr_and_expr = Glob_term.glob_constr * constr_expr option
-type glob_constr_pattern_and_expr = Id.Set.t * glob_constr_and_expr * constr_pattern
+(** Introduction patterns *)
+
+type 'constr intro_pattern_expr =
+  | IntroForthcoming of bool
+  | IntroNaming of Namegen.intro_pattern_naming_expr
+  | IntroAction of 'constr intro_pattern_action_expr
+and 'constr intro_pattern_action_expr =
+  | IntroWildcard
+  | IntroOrAndPattern of 'constr or_and_intro_pattern_expr
+  | IntroInjection of ('constr intro_pattern_expr) CAst.t list
+  | IntroApplyOn of 'constr CAst.t * 'constr intro_pattern_expr CAst.t
+  | IntroRewrite of bool
+and 'constr or_and_intro_pattern_expr =
+  | IntroOrPattern of ('constr intro_pattern_expr) CAst.t list list
+  | IntroAndPattern of ('constr intro_pattern_expr) CAst.t list
+
+(** Bindings *)
+
+type quantified_hypothesis = AnonHyp of int | NamedHyp of Id.t
+
+type 'a explicit_bindings = (quantified_hypothesis * 'a) CAst.t list
+
+type 'a bindings =
+  | ImplicitBindings of 'a list
+  | ExplicitBindings of 'a explicit_bindings
+  | NoBindings
+
+type 'a with_bindings = 'a * 'a bindings
 
 type 'a delayed_open = Environ.env -> Evd.evar_map -> Evd.evar_map * 'a
 
@@ -31,4 +51,4 @@ type delayed_open_constr_with_bindings = EConstr.constr with_bindings delayed_op
 type intro_pattern = delayed_open_constr intro_pattern_expr CAst.t
 type intro_patterns = delayed_open_constr intro_pattern_expr CAst.t list
 type or_and_intro_pattern = delayed_open_constr or_and_intro_pattern_expr CAst.t
-type intro_pattern_naming = intro_pattern_naming_expr CAst.t
+type intro_pattern_naming = Namegen.intro_pattern_naming_expr CAst.t
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 77fe31415..d7de6c4fb 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -99,7 +99,7 @@ let unify_resolve poly flags ((c : raw_hint), clenv) =
   Proofview.Goal.enter begin fun gl ->
   let clenv, c = connect_hint_clenv poly c clenv gl in
   let clenv = clenv_unique_resolver ~flags clenv gl in
-  Clenvtac.clenv_refine false clenv
+  Clenvtac.clenv_refine clenv
   end
 
 let unify_resolve_nodelta poly h = unify_resolve poly auto_unif_flags h
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 4beeaaae0..773fc1520 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -207,7 +207,7 @@ let clenv_unique_resolver_tac with_evars ~flags clenv' =
       try Proofview.tclUNIT (clenv_unique_resolver ~flags clenv' gls)
       with e -> Proofview.tclZERO e
     in resolve >>= fun clenv' ->
-       Clenvtac.clenv_refine with_evars ~with_classes:false clenv'
+       Clenvtac.clenv_refine ~with_evars ~with_classes:false clenv'
   end
 
 let unify_e_resolve poly flags = begin fun gls (c,_,clenv) ->
diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml
index b92bc75bc..e12063fd4 100644
--- a/tactics/contradiction.ml
+++ b/tactics/contradiction.ml
@@ -14,7 +14,6 @@ open Hipattern
 open Tactics
 open Coqlib
 open Reductionops
-open Misctypes
 open Proofview.Notations
 
 module NamedDecl = Context.Named.Declaration
@@ -120,7 +119,7 @@ let contradiction_term (c,lbind as cl) =
     else
       Proofview.tclORELSE
         begin
-          if lbind = NoBindings then
+          if lbind = Tactypes.NoBindings then
             filter_hyp (fun c -> is_negation_of env sigma typ c)
               (fun id -> simplest_elim (mkApp (mkVar id,[|c|])))
           else
diff --git a/tactics/contradiction.mli b/tactics/contradiction.mli
index 2b3a94758..4bb3263fb 100644
--- a/tactics/contradiction.mli
+++ b/tactics/contradiction.mli
@@ -9,7 +9,7 @@
 (************************************************************************)
 
 open EConstr
-open Misctypes
+open Tactypes
 
 val absurd                      : constr -> unit Proofview.tactic
 val contradiction               : constr with_bindings option -> unit Proofview.tactic
diff --git a/tactics/elim.mli b/tactics/elim.mli
index d6b67e5ba..ddfac3f2c 100644
--- a/tactics/elim.mli
+++ b/tactics/elim.mli
@@ -11,12 +11,11 @@
 open Names
 open EConstr
 open Tacticals
-open Misctypes
 open Tactypes
 
 (** Eliminations tactics. *)
 
-val introCaseAssumsThen : evars_flag ->
+val introCaseAssumsThen : Tactics.evars_flag ->
   (intro_patterns -> branch_assumptions -> unit Proofview.tactic) ->
     branch_args -> unit Proofview.tactic
 
diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml
index 176701d99..832014a61 100644
--- a/tactics/eqdecide.ml
+++ b/tactics/eqdecide.ml
@@ -24,11 +24,11 @@ open Tactics
 open Tacticals.New
 open Auto
 open Constr_matching
-open Misctypes
 open Hipattern
 open Proofview.Notations
 open Tacmach.New
 open Coqlib
+open Tactypes
 
 (* This file containts the implementation of the tactics ``Decide
    Equality'' and ``Compare''. They can be used to decide the
@@ -58,14 +58,14 @@ let clear_last =
 
 let choose_eq eqonleft =
   if eqonleft then
-    left_with_bindings false Misctypes.NoBindings
+    left_with_bindings false NoBindings
   else
-    right_with_bindings false Misctypes.NoBindings
+    right_with_bindings false NoBindings
 let choose_noteq eqonleft =
   if eqonleft then
-    right_with_bindings false Misctypes.NoBindings
+    right_with_bindings false NoBindings
   else
-    left_with_bindings false Misctypes.NoBindings
+    left_with_bindings false NoBindings
 
 (* A surgical generalize which selects the right occurrences by hand *)
 (* This prevents issues where c2 is also a subterm of c1 (see e.g. #5449) *)
diff --git a/tactics/equality.ml b/tactics/equality.ml
index d7e697aed..91c577405 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -42,7 +42,7 @@ open Ind_tables
 open Eqschemes
 open Locus
 open Locusops
-open Misctypes
+open Tactypes
 open Proofview.Notations
 open Unification
 open Context.Named.Declaration
@@ -154,7 +154,7 @@ let instantiate_lemma_all frzevars gl c ty l l2r concl =
   let c1 = args.(arglen - 2) in
   let c2 = args.(arglen - 1) in
   let try_occ (evd', c') =
-    Clenvtac.clenv_pose_dependent_evars true {eqclause with evd = evd'}
+    Clenvtac.clenv_pose_dependent_evars ~with_evars:true {eqclause with evd = evd'}
   in
   let flags = make_flags frzevars (Tacmach.New.project gl) rewrite_unif_flags eqclause in
   let occs =
@@ -546,6 +546,12 @@ let apply_special_clear_request clear_flag f =
       e when catchable_exception e -> tclIDTAC
   end
 
+type multi =
+  | Precisely of int
+  | UpTo of int
+  | RepeatStar
+  | RepeatPlus
+
 let general_multi_rewrite with_evars l cl tac =
   let do1 l2r f =
     Proofview.Goal.enter begin fun gl ->
@@ -1037,7 +1043,7 @@ let onEquality with_evars tac (c,lbindc) =
   let t = type_of c in
   let t' = try snd (reduce_to_quantified_ind t) with UserError _ -> t in
   let eq_clause = pf_apply make_clenv_binding gl (c,t') lbindc in
-  let eq_clause' = Clenvtac.clenv_pose_dependent_evars with_evars eq_clause in
+  let eq_clause' = Clenvtac.clenv_pose_dependent_evars ~with_evars eq_clause in
   let eqn = clenv_type eq_clause' in
   let (eq,u,eq_args) = find_this_eq_data_decompose gl eqn in
   tclTHEN
diff --git a/tactics/equality.mli b/tactics/equality.mli
index ccf454c3e..6f3e08ea0 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -15,8 +15,8 @@ open EConstr
 open Environ
 open Ind_tables
 open Locus
-open Misctypes
 open Tactypes
+open Tactics
 (*i*)
 
 type dep_proof_flag = bool (* true = support rewriting dependent proofs *)
@@ -61,6 +61,12 @@ val general_rewrite_in          :
 val general_rewrite_clause :
   orientation -> evars_flag -> ?tac:(unit Proofview.tactic * conditions) -> constr with_bindings -> clause -> unit Proofview.tactic
 
+type multi =
+  | Precisely of int
+  | UpTo of int
+  | RepeatStar
+  | RepeatPlus
+
 val general_multi_rewrite :
   evars_flag -> (bool * multi * clear_flag * delayed_open_constr_with_bindings) list ->
     clause -> (unit Proofview.tactic * conditions) option -> unit Proofview.tactic
diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml
index 5d264058a..f9c4bed35 100644
--- a/tactics/hipattern.ml
+++ b/tactics/hipattern.ml
@@ -263,7 +263,7 @@ open Evar_kinds
 let mkPattern c = snd (Patternops.pattern_of_glob_constr c)
 let mkGApp f args = DAst.make @@ GApp (f, args)
 let mkGHole = DAst.make @@
-  GHole (QuestionMark (Define false,Anonymous), Misctypes.IntroAnonymous, None)
+  GHole (QuestionMark (Define false,Anonymous), Namegen.IntroAnonymous, None)
 let mkGProd id c1 c2 = DAst.make @@
   GProd (Name (Id.of_string id), Explicit, c1, c2)
 let mkGArrow c1 c2 = DAst.make @@
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 102b8e54d..755494c2d 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -26,7 +26,7 @@ open Tacticals.New
 open Tactics
 open Elim
 open Equality
-open Misctypes
+open Tactypes
 open Proofview.Notations
 
 module NamedDecl = Context.Named.Declaration
@@ -332,7 +332,7 @@ let rec tclMAP_i allow_conj n tacfun = function
           (tacfun (get_names allow_conj a))
           (tclMAP_i allow_conj (n-1) tacfun l)
 
-let remember_first_eq id x = if !x == MoveLast then x := MoveAfter id
+let remember_first_eq id x = if !x == Logic.MoveLast then x := Logic.MoveAfter id
 
 (* invariant: ProjectAndApply is responsible for erasing the clause
    which it is given as input
@@ -375,7 +375,7 @@ let projectAndApply as_mode thin avoid id eqname names depids =
       [if as_mode then clear [id] else tclIDTAC;
        (tclMAP_i (false,false) neqns (function (idopt,_) ->
 	 tclTRY (tclTHEN
-	   (intro_move_avoid idopt avoid MoveLast)
+           (intro_move_avoid idopt avoid Logic.MoveLast)
 	   (* try again to substitute and if still not a variable after *)
 	   (* decomposition, arbitrarily try to rewrite RL !? *)
 	   (tclTRY (onLastHypId (substHypIfVariable (fun id -> subst_hyp false id))))))
@@ -404,7 +404,7 @@ let nLastDecls i tac =
 let rewrite_equations as_mode othin neqns names ba =
   Proofview.Goal.enter begin fun gl ->
   let (depids,nodepids) = split_dep_and_nodep ba.Tacticals.assums gl in
-  let first_eq = ref MoveLast in
+  let first_eq = ref Logic.MoveLast in
   let avoid = if as_mode then Id.Set.of_list (List.map NamedDecl.get_id nodepids) else Id.Set.empty in
   match othin with
     | Some thin ->
@@ -416,20 +416,20 @@ let rewrite_equations as_mode othin neqns names ba =
              (nLastDecls neqns (fun ctx -> clear (ids_of_named_context ctx)));
 	     tclMAP_i (true,false) neqns (fun (idopt,names) ->
                (tclTHEN
-		 (intro_move_avoid idopt avoid MoveLast)
+                 (intro_move_avoid idopt avoid Logic.MoveLast)
 		 (onLastHypId (fun id ->
 		   tclTRY (projectAndApply as_mode thin avoid id first_eq names depids)))))
 	       names;
 	     tclMAP (fun d -> tclIDTAC >>= fun () -> (* delay for [first_eq]. *)
                let idopt = if as_mode then Some (NamedDecl.get_id d) else None in
-	       intro_move idopt (if thin then MoveLast else !first_eq))
+               intro_move idopt (if thin then Logic.MoveLast else !first_eq))
 	       nodepids;
 	     (tclMAP (fun d -> tclTRY (clear [NamedDecl.get_id d])) depids)]
     | None ->
         (* simple inversion *)
         if as_mode then
           tclMAP_i (false,true) neqns (fun (idopt,_) ->
-	    intro_move idopt MoveLast) names
+            intro_move idopt Logic.MoveLast) names
         else
           (tclTHENLIST
              [tclDO neqns intro;
diff --git a/tactics/inv.mli b/tactics/inv.mli
index 9d4ffdd7b..bbd1f3352 100644
--- a/tactics/inv.mli
+++ b/tactics/inv.mli
@@ -10,7 +10,6 @@
 
 open Names
 open EConstr
-open Misctypes
 open Tactypes
 
 type inversion_status = Dep of constr option | NoDep
diff --git a/tactics/leminv.mli b/tactics/leminv.mli
index 2337a7901..f42e5a8b0 100644
--- a/tactics/leminv.mli
+++ b/tactics/leminv.mli
@@ -11,7 +11,7 @@
 open Names
 open EConstr
 open Constrexpr
-open Misctypes
+open Tactypes
 
 val lemInv_clause :
   quantified_hypothesis -> constr -> Id.t list -> unit Proofview.tactic
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 732d06f8a..f34c83ae7 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -159,8 +159,6 @@ type branch_assumptions = {
   ba        : branch_args;       (* the branch args *)
   assums    : named_context}   (* the list of assumptions introduced *)
 
-open Misctypes
-
 let fix_empty_or_and_pattern nv l =
   (* 1- The syntax does not distinguish between "[ ]" for one clause with no
      names and "[ ]" for no clause at all *)
@@ -194,7 +192,7 @@ let check_or_and_pattern_size ?loc check_and names branchsigns =
         if not (Int.equal p p1 || Int.equal p p2) then err1 p1 p2;
         if Int.equal p p1 then
           IntroAndPattern
-            (List.extend branchsigns.(0) (CAst.make @@ IntroNaming IntroAnonymous) l)
+            (List.extend branchsigns.(0) (CAst.make @@ IntroNaming Namegen.IntroAnonymous) l)
         else
           names
       else
@@ -225,7 +223,7 @@ let compute_induction_names_gen check_and branchletsigns = function
 let compute_induction_names = compute_induction_names_gen true
 
 (* Compute the let-in signature of case analysis or standard induction scheme *)
-let compute_constructor_signatures isrec ((_,k as ity),u) =
+let compute_constructor_signatures ~rec_flag ((_,k as ity),u) =
   let rec analrec c recargs =
     match Constr.kind c, recargs with
     | Prod (_,_,c), recarg::rest ->
@@ -233,7 +231,7 @@ let compute_constructor_signatures isrec ((_,k as ity),u) =
         begin match Declareops.dest_recarg recarg with
         | Norec | Imbr _  -> true :: rest
         | Mrec (_,j)  ->
-            if isrec && Int.equal j k then true :: true :: rest
+            if rec_flag && Int.equal j k then true :: true :: rest
             else true :: rest
         end
     | LetIn (_,_,_,c), rest -> false :: analrec c rest
@@ -636,7 +634,7 @@ module New = struct
   (* Find the right elimination suffix corresponding to the sort of the goal *)
   (* c should be of type A1->.. An->B with B an inductive definition *)
   let general_elim_then_using mk_elim
-      isrec allnames tac predicate ind (c, t) =
+      rec_flag allnames tac predicate ind (c, t) =
     Proofview.Goal.enter begin fun gl ->
     let sigma, elim = mk_elim ind gl in
     let ind = on_snd (fun u -> EInstance.kind sigma u) ind in
@@ -665,7 +663,7 @@ module New = struct
             (str "The elimination combinator " ++ str name_elim ++ str " is unknown.")
     in
     let elimclause' = clenv_fchain ~with_univs:false indmv elimclause indclause in
-    let branchsigns = compute_constructor_signatures isrec ind in
+    let branchsigns = compute_constructor_signatures ~rec_flag ind in
     let brnames = compute_induction_names_gen false branchsigns allnames in
     let flags = Unification.elim_flags () in
     let elimclause' =
@@ -688,7 +686,7 @@ module New = struct
     in
     let branchtacs = List.init (Array.length branchsigns) after_tac in
     Proofview.tclTHEN
-      (Clenvtac.clenv_refine false clenv')
+      (Clenvtac.clenv_refine clenv')
       (Proofview.tclEXTEND [] tclIDTAC branchtacs)
     end) end
 
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index cbaf691f1..1e66c2b0b 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -14,7 +14,6 @@ open EConstr
 open Evd
 open Proof_type
 open Locus
-open Misctypes
 open Tactypes
 
 (** Tacticals i.e. functions from tactics to tactics. *)
@@ -124,7 +123,7 @@ val fix_empty_or_and_pattern : int ->
   delayed_open_constr or_and_intro_pattern_expr ->
   delayed_open_constr or_and_intro_pattern_expr
 
-val compute_constructor_signatures : rec_flag -> inductive * 'a -> bool list array
+val compute_constructor_signatures : rec_flag:bool -> inductive * 'a -> bool list array
 
 (** Useful for [as intro_pattern] modifier *)
 val compute_induction_names :
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index b571b347d..67170d2cf 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -43,7 +43,7 @@ open Pretype_errors
 open Unification
 open Locus
 open Locusops
-open Misctypes
+open Tactypes
 open Proofview.Notations
 open Context.Named.Declaration
 
@@ -1153,6 +1153,11 @@ let tactic_infer_flags with_evar = {
   Pretyping.fail_evar = not with_evar;
   Pretyping.expand_evars = true }
 
+type evars_flag = bool     (* true = pose evars       false = fail on evars *)
+type rec_flag = bool       (* true = recursive        false = not recursive *)
+type advanced_flag = bool  (* true = advanced         false = basic *)
+type clear_flag = bool option (* true = clear hyp, false = keep hyp, None = use default *)
+
 type 'a core_destruction_arg =
   | ElimOnConstr of 'a
   | ElimOnIdent of lident
@@ -1281,7 +1286,7 @@ let do_replace id = function
 
 let clenv_refine_in ?(sidecond_first=false) with_evars ?(with_classes=true) 
     targetid id sigma0 clenv tac =
-  let clenv = Clenvtac.clenv_pose_dependent_evars with_evars clenv in
+  let clenv = Clenvtac.clenv_pose_dependent_evars ~with_evars clenv in
   let clenv =
     if with_classes then
       { clenv with evd = Typeclasses.resolve_typeclasses 
@@ -2258,7 +2263,7 @@ let intro_or_and_pattern ?loc with_evars bracketed ll thin tac id =
   let c = mkVar id in
   let t = Tacmach.New.pf_unsafe_type_of gl c in
   let (ind,t) = Tacmach.New.pf_reduce_to_quantified_ind gl t in
-  let branchsigns = compute_constructor_signatures false ind in
+  let branchsigns = compute_constructor_signatures ~rec_flag:false ind in
   let nv_with_let = Array.map List.length branchsigns in
   let ll = fix_empty_or_and_pattern (Array.length branchsigns) ll in
   let ll = get_and_check_or_and_pattern ?loc ll branchsigns in
@@ -4196,7 +4201,7 @@ let induction_tac with_evars params indvars elim =
   let elimclause' = recolle_clenv i params indvars elimclause gl in
   (* one last resolution (useless?) *)
   let resolved = clenv_unique_resolver ~flags:(elim_flags ()) elimclause' gl in
-  Clenvtac.clenv_refine with_evars resolved
+  Clenvtac.clenv_refine ~with_evars resolved
   end
 
 (* Apply induction "in place" taking into account dependent
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index b17330f13..8d4302450 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -18,7 +18,6 @@ open Clenv
 open Redexpr
 open Pattern
 open Unification
-open Misctypes
 open Tactypes
 open Locus
 open Ltac_pretype
@@ -56,8 +55,8 @@ val find_intro_names : rel_context -> goal sigma -> Id.t list
 
 val intro                : unit Proofview.tactic
 val introf               : unit Proofview.tactic
-val intro_move        : Id.t option -> Id.t move_location -> unit Proofview.tactic
-val intro_move_avoid  : Id.t option -> Id.Set.t -> Id.t move_location -> unit Proofview.tactic
+val intro_move        : Id.t option -> Id.t Logic.move_location -> unit Proofview.tactic
+val intro_move_avoid  : Id.t option -> Id.Set.t -> Id.t Logic.move_location -> unit Proofview.tactic
 
   (** [intro_avoiding idl] acts as intro but prevents the new Id.t
      to belong to [idl] *)
@@ -91,6 +90,11 @@ val intros_clearing      : bool list -> unit Proofview.tactic
 val try_intros_until :
   (Id.t -> unit Proofview.tactic) -> quantified_hypothesis -> unit Proofview.tactic
 
+type evars_flag = bool     (* true = pose evars       false = fail on evars *)
+type rec_flag = bool       (* true = recursive        false = not recursive *)
+type advanced_flag = bool  (* true = advanced         false = basic *)
+type clear_flag = bool option (* true = clear hyp, false = keep hyp, None = use default *)
+
 (** Apply a tactic on a quantified hypothesis, an hypothesis in context
    or a term with bindings *)
 
@@ -117,11 +121,11 @@ val use_clear_hyp_by_default : unit -> bool
 (** {6 Introduction tactics with eliminations. } *)
 
 val intro_patterns : evars_flag -> intro_patterns -> unit Proofview.tactic
-val intro_patterns_to : evars_flag -> Id.t move_location -> intro_patterns ->
+val intro_patterns_to : evars_flag -> Id.t Logic.move_location -> intro_patterns ->
   unit Proofview.tactic
-val intro_patterns_bound_to : evars_flag -> int -> Id.t move_location -> intro_patterns ->
+val intro_patterns_bound_to : evars_flag -> int -> Id.t Logic.move_location -> intro_patterns ->
   unit Proofview.tactic
-val intro_pattern_to : evars_flag -> Id.t move_location -> delayed_open_constr intro_pattern_expr ->
+val intro_pattern_to : evars_flag -> Id.t Logic.move_location -> delayed_open_constr intro_pattern_expr ->
   unit Proofview.tactic
 
 (** Implements user-level "intros", with [] standing for "**" *)
@@ -188,7 +192,7 @@ val apply_clear_request : clear_flag -> bool -> constr -> unit Proofview.tactic
 
 val specialize    : constr with_bindings -> intro_pattern option -> unit Proofview.tactic
 
-val move_hyp      : Id.t -> Id.t move_location -> unit Proofview.tactic
+val move_hyp      : Id.t -> Id.t Logic.move_location -> unit Proofview.tactic
 val rename_hyp    : (Id.t * Id.t) list -> unit Proofview.tactic
 
 val revert        : Id.t list -> unit Proofview.tactic
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index 8b56275c7..ee578669c 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -24,7 +24,8 @@ open Globnames
 open Inductiveops
 open Tactics
 open Ind_tables
-open Misctypes
+open Namegen
+open Tactypes
 open Proofview.Notations
 
 module RelDecl = Context.Rel.Declaration
diff --git a/vernac/classes.ml b/vernac/classes.ml
index 946a7bb32..8cf3895fb 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -145,7 +145,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance)
 	  (fun avoid (clname, _) ->
 	    match clname with
             | Some cl ->
-		let t = CAst.make @@ CHole (None, Misctypes.IntroAnonymous, None) in
+                let t = CAst.make @@ CHole (None, Namegen.IntroAnonymous, None) in
 		  t, avoid
 	    | None -> failwith ("new instance: under-applied typeclass"))
 	  cl
@@ -255,7 +255,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance)
 			   k.cl_projs;
 			 c :: props, rest'
 		     with Not_found ->
-		       ((CAst.make @@ CHole (None(* Some Evar_kinds.GoalEvar *), Misctypes.IntroAnonymous, None)) :: props), rest
+                       ((CAst.make @@ CHole (None(* Some Evar_kinds.GoalEvar *), Namegen.IntroAnonymous, None)) :: props), rest
 		   else props, rest)
 		([], props) k.cl_props
 	    in
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/g_proofs.ml4 b/vernac/g_proofs.ml4
index a3806ff68..4b11276af 100644
--- a/vernac/g_proofs.ml4
+++ b/vernac/g_proofs.ml4
@@ -8,10 +8,10 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
+open Glob_term
 open Constrexpr
 open Vernacexpr
 open Proof_global
-open Misctypes
 
 open Pcoq
 open Pcoq.Prim
diff --git a/vernac/g_vernac.ml4 b/vernac/g_vernac.ml4
index b6523981c..3a59242de 100644
--- a/vernac/g_vernac.ml4
+++ b/vernac/g_vernac.ml4
@@ -12,6 +12,7 @@ open Pp
 open CErrors
 open Util
 open Names
+open Glob_term
 open Vernacexpr
 open Constrexpr
 open Constrexpr_ops
@@ -19,7 +20,7 @@ open Extend
 open Decl_kinds
 open Declaremods
 open Declarations
-open Misctypes
+open Namegen
 open Tok (* necessary for camlp5 *)
 
 open Pcoq
@@ -338,7 +339,7 @@ GEXTEND Gram
   ;
   type_cstr:
     [ [ ":"; c=lconstr -> c
-      | -> CAst.make ~loc:!@loc @@ CHole (None, Misctypes.IntroAnonymous, None) ] ]
+      | -> CAst.make ~loc:!@loc @@ CHole (None, IntroAnonymous, None) ] ]
   ;
   (* Inductive schemes *)
   scheme:
@@ -394,7 +395,7 @@ GEXTEND Gram
 	     (None,DefExpr(id,mkCLambdaN ~loc:!@loc l b,None)) ] ]
   ;
   record_binder:
-    [ [ id = name -> (None,AssumExpr(id, CAst.make ~loc:!@loc @@ CHole (None, Misctypes.IntroAnonymous, None)))
+    [ [ id = name -> (None,AssumExpr(id, CAst.make ~loc:!@loc @@ CHole (None, IntroAnonymous, None)))
       | id = name; f = record_binder_body -> f id ] ]
   ;
   assum_list:
@@ -413,7 +414,7 @@ GEXTEND Gram
       t= [ coe = of_type_with_opt_coercion; c = lconstr ->
 	            fun l id -> (not (Option.is_empty coe),(id,mkCProdN ~loc:!@loc l c))
             |  ->
-		 fun l id -> (false,(id,mkCProdN ~loc:!@loc l (CAst.make ~loc:!@loc @@ CHole (None, Misctypes.IntroAnonymous, None)))) ]
+                 fun l id -> (false,(id,mkCProdN ~loc:!@loc l (CAst.make ~loc:!@loc @@ CHole (None, IntroAnonymous, None)))) ]
 	 -> t l
      ]]
 ;
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/misctypes.ml b/vernac/misctypes.ml
new file mode 100644
index 000000000..ae725efaa
--- /dev/null
+++ b/vernac/misctypes.ml
@@ -0,0 +1,75 @@
+(* Compat module, to be removed in 8.10 *)
+open Names
+
+type lident = Names.lident
+[@@ocaml.deprecated "use [Names.lident"]
+type lname = Names.lname
+[@@ocaml.deprecated "use [Names.lname]"]
+type lstring = Names.lstring
+[@@ocaml.deprecated "use [Names.lstring]"]
+
+type 'a or_by_notation_r = 'a Constrexpr.or_by_notation_r =
+  | AN of 'a [@ocaml.deprecated "use version in [Constrexpr]"]
+  | ByNotation of (string * string option) [@ocaml.deprecated "use version in [Constrexpr]"]
+[@@ocaml.deprecated "use [Constrexpr.or_by_notation_r]"]
+
+type 'a or_by_notation = 'a Constrexpr.or_by_notation
+[@@ocaml.deprecated "use [Constrexpr.or_by_notation]"]
+
+type intro_pattern_naming_expr = Namegen.intro_pattern_naming_expr =
+  | IntroIdentifier of Id.t [@ocaml.deprecated "Use version in [Evarutil]"]
+  | IntroFresh of Id.t [@ocaml.deprecated "Use version in [Evarutil]"]
+  | IntroAnonymous [@ocaml.deprecated "Use version in [Evarutil]"]
+[@@ocaml.deprecated "use [Evarutil.intro_pattern_naming_expr]"]
+
+type 'a or_var = 'a Locus.or_var =
+  | ArgArg of 'a [@ocaml.deprecated "Use version in [Locus]"]
+  | ArgVar of Names.lident [@ocaml.deprecated "Use version in [Locus]"]
+[@@ocaml.deprecated "use [Locus.or_var]"]
+
+type quantified_hypothesis = Tactypes.quantified_hypothesis =
+    AnonHyp of int [@ocaml.deprecated "Use version in [Tactypes]"]
+  | NamedHyp of Id.t [@ocaml.deprecated "Use version in [Tactypes]"]
+[@@ocaml.deprecated "use [Tactypes.quantified_hypothesis]"]
+
+type multi = Equality.multi =
+  | Precisely of int [@ocaml.deprecated "use version in [Equality]"]
+  | UpTo of int [@ocaml.deprecated "use version in [Equality]"]
+  | RepeatStar [@ocaml.deprecated "use version in [Equality]"]
+  | RepeatPlus [@ocaml.deprecated "use version in [Equality]"]
+[@@ocaml.deprecated "use [Equality.multi]"]
+
+type 'a bindings = 'a Tactypes.bindings =
+  | ImplicitBindings of 'a list [@ocaml.deprecated "use version in [Tactypes]"]
+  | ExplicitBindings of 'a Tactypes.explicit_bindings [@ocaml.deprecated "use version in [Tactypes]"]
+  | NoBindings [@ocaml.deprecated "use version in [Tactypes]"]
+[@@ocaml.deprecated "use [Tactypes.bindings]"]
+
+type 'constr intro_pattern_expr = 'constr Tactypes.intro_pattern_expr =
+  | IntroForthcoming of bool [@ocaml.deprecated "use version in [Tactypes]"]
+  | IntroNaming of Namegen.intro_pattern_naming_expr [@ocaml.deprecated "use version in [Tactypes]"]
+  | IntroAction of 'constr Tactypes.intro_pattern_action_expr [@ocaml.deprecated "use version in [Tactypes]"]
+and 'constr intro_pattern_action_expr = 'constr Tactypes.intro_pattern_action_expr =
+  | IntroWildcard [@ocaml.deprecated "use [Tactypes]"]
+  | IntroOrAndPattern of 'constr Tactypes.or_and_intro_pattern_expr [@ocaml.deprecated "use [Tactypes]"]
+  | IntroInjection of ('constr intro_pattern_expr) CAst.t list [@ocaml.deprecated "use [Tactypes]"]
+  | IntroApplyOn of 'constr CAst.t * 'constr intro_pattern_expr CAst.t [@ocaml.deprecated "use [Tactypes]"]
+  | IntroRewrite of bool [@ocaml.deprecated "use [Tactypes]"]
+and 'constr or_and_intro_pattern_expr = 'constr Tactypes.or_and_intro_pattern_expr =
+  | IntroOrPattern of ('constr intro_pattern_expr) CAst.t list list [@ocaml.deprecated "use [Tactypes]"]
+  | IntroAndPattern of ('constr intro_pattern_expr) CAst.t list [@ocaml.deprecated "use [Tactypes]"]
+[@@ocaml.deprecated "use version in [Tactypes]"]
+
+type 'id move_location = 'id Logic.move_location =
+  | MoveAfter of 'id [@ocaml.deprecated "use version in [Logic]"]
+  | MoveBefore of 'id [@ocaml.deprecated "use version in [Logic]"]
+  | MoveFirst [@ocaml.deprecated "use version in [Logic]"]
+  | MoveLast [@ocaml.deprecated "use version in [Logic]"]
+[@@ocaml.deprecated "use version in [Logic]"]
+
+type 'a cast_type = 'a Glob_term.cast_type =
+  | CastConv of 'a [@ocaml.deprecated "use version in [Glob_term]"]
+  | CastVM of 'a [@ocaml.deprecated "use version in [Glob_term]"]
+  | CastCoerce [@ocaml.deprecated "use version in [Glob_term]"]
+  | CastNative of 'a [@ocaml.deprecated "use version in [Glob_term]"]
+[@@ocaml.deprecated "use version in [Glob_term]"]
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 :
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index 5490b9ce5..d0c423650 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -286,7 +286,7 @@ open Pputils
     prlist_strict (pr_module_vardecls pr_c) l
 
   let pr_type_option pr_c = function
-    | { v = CHole (k, Misctypes.IntroAnonymous, _) } -> mt()
+    | { v = CHole (k, Namegen.IntroAnonymous, _) } -> mt()
     | _ as c -> brk(0,2) ++ str" :" ++ pr_c c
 
   let pr_decl_notation prc ({loc; v=ntn},c,scopt) =
diff --git a/vernac/record.ml b/vernac/record.ml
index e6a3afe4e..940859723 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -96,7 +96,7 @@ let binder_of_decl = function
   | Vernacexpr.AssumExpr(n,t) -> (n,None,t)
   | Vernacexpr.DefExpr(n,c,t) ->
     (n,Some c, match t with Some c -> c
-                          | None   -> CAst.make ?loc:n.CAst.loc @@ CHole (None, Misctypes.IntroAnonymous, None))
+                          | None   -> CAst.make ?loc:n.CAst.loc @@ CHole (None, Namegen.IntroAnonymous, None))
 
 let binders_of_decls = List.map binder_of_decl
 
diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib
index 39c313ac7..356951b69 100644
--- a/vernac/vernac.mllib
+++ b/vernac/vernac.mllib
@@ -31,3 +31,5 @@ Vernacstate
 Mltop
 Topfmt
 Vernacentries
+
+Misctypes
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 7f6270df1..94eb45fd3 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -29,7 +29,6 @@ open Decl_kinds
 open Constrexpr
 open Redexpr
 open Lemmas
-open Misctypes
 open Locality
 open Vernacinterp
 
@@ -637,7 +636,7 @@ let vernac_scheme l =
 let vernac_combined_scheme lid l =
   if Dumpglob.dump () then
     (Dumpglob.dump_definition lid false "def";
-     List.iter (fun {loc;v=id} -> dump_global (make ?loc @@ Misctypes.AN (make ?loc @@ Ident id))) l);
+     List.iter (fun {loc;v=id} -> dump_global (make ?loc @@ AN (make ?loc @@ Ident id))) l);
  Indschemes.do_combined_scheme lid l
 
 let vernac_universe ~atts l =
diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli
index f6199e820..3c88a3443 100644
--- a/vernac/vernacentries.mli
+++ b/vernac/vernacentries.mli
@@ -8,9 +8,7 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-open Misctypes
-
-val dump_global : Libnames.reference or_by_notation -> unit
+val dump_global : Libnames.reference Constrexpr.or_by_notation -> unit
 
 (** Vernacular entries *)
 val vernac_require :
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index 9e8dfc4f8..5acac9e25 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -9,7 +9,6 @@
 (************************************************************************)
 
 open Names
-open Misctypes
 open Constrexpr
 open Libnames