[api] Misctypes removal: several moves:

- move_location to proofs/logic.
- intro_pattern_naming to Namegen.

89 files changed, 322 insertions, 341 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/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/interp/constrexpr.ml b/interp/constrexpr.ml
index d6b395e01..60f2c683a 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 } *)
@@ -94,11 +93,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
+  | 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 057e10c00..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
@@ -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
@@ -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/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/tactypes.ml b/interp/tactypes.ml
index 83e42be89..f19abefee 100644
--- a/interp/tactypes.ml
+++ b/interp/tactypes.ml
@@ -15,7 +15,35 @@
 open Names
 open Constrexpr
 open Pattern
-open Misctypes
+
+(** 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
 
 (** In globalize tactics, we need to keep the initial [constr_expr] to recompute
    in the environment by the effective calls to Intro, Inversion, etc 
@@ -31,4 +59,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/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/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/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..24d1a40c2 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -15,7 +15,7 @@ open Indfun_common
 open Indfun
 open Genarg
 open Stdarg
-open Misctypes
+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..1070b30a1 100644
--- a/plugins/ltac/coretactics.ml4
+++ b/plugins/ltac/coretactics.ml4
@@ -11,10 +11,12 @@
 open Util
 open Locus
 open Misctypes
+open Tactypes
 open Genredexpr
 open Stdarg
 open Extraargs
 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/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..de9ff2875 100644
--- a/plugins/ltac/g_ltac.ml4
+++ b/plugins/ltac/g_ltac.ml4
@@ -12,9 +12,11 @@ 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 *)
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 038d55e4b..c91c160f0 100644
--- a/plugins/ltac/g_tactic.ml4
+++ b/plugins/ltac/g_tactic.ml4
@@ -12,12 +12,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
 
diff --git a/plugins/ltac/pltac.mli b/plugins/ltac/pltac.mli
index de23d2f8e..a75ca8ecb 100644
--- a/plugins/ltac/pltac.mli
+++ b/plugins/ltac/pltac.mli
@@ -16,6 +16,7 @@ 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
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index 894d91258..7b72a4bf9 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -20,6 +20,7 @@ open Stdarg
 open Libnames
 open Notation_gram
 open Misctypes
+open Tactypes
 open Locus
 open Decl_kinds
 open Genredexpr
@@ -749,7 +750,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..c14874d6c 100644
--- a/plugins/ltac/pptactic.mli
+++ b/plugins/ltac/pptactic.mli
@@ -19,6 +19,7 @@ open Environ
 open Constrexpr
 open Notation_gram
 open Tacexpr
+open Tactypes
 
 type 'a grammar_tactic_prod_item_expr =
 | TacTerm of string
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.mli b/plugins/ltac/tacarg.mli
index 59473a5e5..1abe7cd6f 100644
--- a/plugins/ltac/tacarg.mli
+++ b/plugins/ltac/tacarg.mli
@@ -11,7 +11,7 @@
 open Genarg
 open Tacexpr
 open Constrexpr
-open Misctypes
+open Tactypes
 
 (** Generic arguments based on Ltac. *)
 
diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml
index 3812a2ba2..27acbb629 100644
--- a/plugins/ltac/taccoerce.ml
+++ b/plugins/ltac/taccoerce.ml
@@ -13,6 +13,8 @@ open Names
 open Constr
 open EConstr
 open Misctypes
+open Namegen
+open Tactypes
 open Genarg
 open Stdarg
 open Geninterp
diff --git a/plugins/ltac/taccoerce.mli b/plugins/ltac/taccoerce.mli
index 5185217cd..31bce197b 100644
--- a/plugins/ltac/taccoerce.mli
+++ b/plugins/ltac/taccoerce.mli
@@ -14,6 +14,7 @@ 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 +57,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
 
diff --git a/plugins/ltac/tacexpr.ml b/plugins/ltac/tacexpr.ml
index d6f7a461b..289434d8a 100644
--- a/plugins/ltac/tacexpr.ml
+++ b/plugins/ltac/tacexpr.ml
@@ -16,6 +16,7 @@ open Genredexpr
 open Genarg
 open Pattern
 open Misctypes
+open Tactypes
 open Locus
 
 type ltac_constant = KerName.t
@@ -75,7 +76,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 ... *)
 
@@ -134,7 +135,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 +153,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
diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli
index d6f7a461b..42f6883b4 100644
--- a/plugins/ltac/tacexpr.mli
+++ b/plugins/ltac/tacexpr.mli
@@ -17,6 +17,7 @@ open Genarg
 open Pattern
 open Misctypes
 open Locus
+open Tactypes
 
 type ltac_constant = KerName.t
 
@@ -75,7 +76,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 ... *)
 
@@ -134,7 +135,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 +153,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
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index 9ad9e1520..2a5c38024 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -28,6 +28,8 @@ 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..04c93eae3 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
@@ -36,6 +37,7 @@ 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..e18f6ab19 100644
--- a/plugins/ltac/tacinterp.mli
+++ b/plugins/ltac/tacinterp.mli
@@ -15,6 +15,7 @@ open Tacexpr
 open Genarg
 open Redexpr
 open Misctypes
+open Tactypes
 
 val ltac_trace_info : ltac_trace Exninfo.t
 
diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml
index 50bf687b1..0b86a68b0 100644
--- a/plugins/ltac/tacsubst.ml
+++ b/plugins/ltac/tacsubst.ml
@@ -15,6 +15,7 @@ open Genarg
 open Stdarg
 open Tacarg
 open Misctypes
+open Tactypes
 open Globnames
 open Genredexpr
 open Patternops
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/tauto.ml b/plugins/ltac/tauto.ml
index 8eeb8903e..368c20469 100644
--- a/plugins/ltac/tauto.ml
+++ b/plugins/ltac/tauto.ml
@@ -94,7 +94,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 +175,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
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/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index 3f6503e73..ea7216832 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -184,7 +184,7 @@ 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 +254,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 +861,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..9d7fc254c 100644
--- a/plugins/ssr/ssrparser.ml4
+++ b/plugins/ssr/ssrparser.ml4
@@ -29,6 +29,8 @@ open Extraargs
 open Ppconstr
 
 open Misctypes
+open Namegen
+open Tactypes
 open Decl_kinds
 open Constrexpr
 open Constrexpr_ops
@@ -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/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/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/library/misctypes.ml b/pretyping/misctypes.ml
index 7cd1a83be..c66c9b1b8 100644
--- a/library/misctypes.ml
+++ b/pretyping/misctypes.ml
@@ -10,55 +10,6 @@
 
 open Names
 
-(** 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 *)
-
-(** 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 =
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/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/printing/ppconstr.ml b/printing/ppconstr.ml
index e877b3c63..02204495a 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -15,15 +15,16 @@ 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 +229,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} =
@@ -363,7 +364,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 +458,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 +593,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 +644,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/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/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/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/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 c91758787..1033c56c9 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -43,6 +43,7 @@ open Eqschemes
 open Locus
 open Locusops
 open Misctypes
+open Tactypes
 open Proofview.Notations
 open Unification
 open Context.Named.Declaration
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..53a02f89b 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
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index b571b347d..cf07532c0 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -44,6 +44,7 @@ open Unification
 open Locus
 open Locusops
 open Misctypes
+open Tactypes
 open Proofview.Notations
 open Context.Named.Declaration
 
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index b17330f13..086442e42 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -56,8 +56,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] *)
@@ -117,11 +117,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 +188,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/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..59449d07a 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
@@ -20,6 +21,7 @@ open Decl_kinds
 open Declaremods
 open Declarations
 open Misctypes
+open Namegen
 open Tok (* necessary for camlp5 *)
 
 open Pcoq
@@ -338,7 +340,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 +396,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 +415,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/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