Merge PR #7677: [api] Remove Misctypes

28 files changed, 118 insertions, 79 deletions

diff --git a/plugins/ltac/coretactics.ml4 b/plugins/ltac/coretactics.ml4
index faa9e413bb..61525cb49d 100644
--- a/plugins/ltac/coretactics.ml4
+++ b/plugins/ltac/coretactics.ml4
@@ -10,11 +10,13 @@
 
 open Util
 open Locus
-open Misctypes
+open Tactypes
 open Genredexpr
 open Stdarg
 open Extraargs
+open Tacarg
 open Names
+open Logic
 
 DECLARE PLUGIN "ltac_plugin"
 
diff --git a/plugins/ltac/evar_tactics.ml b/plugins/ltac/evar_tactics.ml
index ea8dcf57dd..84f13d2131 100644
--- a/plugins/ltac/evar_tactics.ml
+++ b/plugins/ltac/evar_tactics.ml
@@ -92,7 +92,7 @@ let let_evar name typ =
       Namegen.next_ident_away_in_goal id (Termops.vars_of_env env)
     | Name.Name id -> id
     in
-    let (sigma, evar) = Evarutil.new_evar env sigma ~src ~naming:(Misctypes.IntroFresh id) typ in
+    let (sigma, evar) = Evarutil.new_evar env sigma ~src ~naming:(Namegen.IntroFresh id) typ in
     Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
     (Tactics.letin_tac None (Name.Name id) evar None Locusops.nowhere)
   end
diff --git a/plugins/ltac/extraargs.ml4 b/plugins/ltac/extraargs.ml4
index 4e7c8b754f..dae2582bd4 100644
--- a/plugins/ltac/extraargs.ml4
+++ b/plugins/ltac/extraargs.ml4
@@ -19,7 +19,6 @@ open Tacmach
 open Tacexpr
 open Taccoerce
 open Tacinterp
-open Misctypes
 open Locus
 
 (** Adding scopes for generic arguments not defined through ARGUMENT EXTEND *)
@@ -35,7 +34,7 @@ let () = create_generic_quotation "ident" Pcoq.Prim.ident Stdarg.wit_ident
 let () = create_generic_quotation "reference" Pcoq.Prim.reference Stdarg.wit_ref
 let () = create_generic_quotation "uconstr" Pcoq.Constr.lconstr Stdarg.wit_uconstr
 let () = create_generic_quotation "constr" Pcoq.Constr.lconstr Stdarg.wit_constr
-let () = create_generic_quotation "ipattern" Pltac.simple_intropattern Stdarg.wit_intro_pattern
+let () = create_generic_quotation "ipattern" Pltac.simple_intropattern wit_intro_pattern
 let () = create_generic_quotation "open_constr" Pcoq.Constr.lconstr Stdarg.wit_open_constr
 let () =
   let inject (loc, v) = Tacexpr.Tacexp v in
diff --git a/plugins/ltac/extraargs.mli b/plugins/ltac/extraargs.mli
index ff697e3c75..7371478848 100644
--- a/plugins/ltac/extraargs.mli
+++ b/plugins/ltac/extraargs.mli
@@ -12,7 +12,6 @@ open Tacexpr
 open Names
 open Constrexpr
 open Glob_term
-open Misctypes
 
 val wit_orient : bool Genarg.uniform_genarg_type
 val orient : bool Pcoq.Gram.entry
@@ -20,9 +19,9 @@ val pr_orient : bool -> Pp.t
 
 val wit_rename : (Id.t * Id.t) Genarg.uniform_genarg_type
 
-val occurrences : (int list or_var) Pcoq.Gram.entry
-val wit_occurrences : (int list or_var, int list or_var, int list) Genarg.genarg_type
-val pr_occurrences : int list or_var -> Pp.t
+val occurrences : (int list Locus.or_var) Pcoq.Gram.entry
+val wit_occurrences : (int list Locus.or_var, int list Locus.or_var, int list) Genarg.genarg_type
+val pr_occurrences : int list Locus.or_var -> Pp.t
 val occurrences_of : int list -> Locus.occurrences
 
 val wit_natural : int Genarg.uniform_genarg_type
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index cb7183638e..f2899ab63c 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 ed54320a59..d7d642e500 100644
--- a/plugins/ltac/g_ltac.ml4
+++ b/plugins/ltac/g_ltac.ml4
@@ -12,9 +12,10 @@ DECLARE PLUGIN "ltac_plugin"
 
 open Util
 open Pp
+open Glob_term
 open Constrexpr
 open Tacexpr
-open Misctypes
+open Namegen
 open Genarg
 open Genredexpr
 open Tok (* necessary for camlp5 *)
@@ -26,7 +27,7 @@ open Pcoq.Constr
 open Pvernac.Vernac_
 open Pltac
 
-let fail_default_value = ArgArg 0
+let fail_default_value = Locus.ArgArg 0
 
 let arg_of_expr = function
     TacArg (loc,a) -> a
@@ -34,7 +35,7 @@ let arg_of_expr = function
 
 let genarg_of_unit () = in_gen (rawwit Stdarg.wit_unit) ()
 let genarg_of_int n = in_gen (rawwit Stdarg.wit_int) n
-let genarg_of_ipattern pat = in_gen (rawwit Stdarg.wit_intro_pattern) pat
+let genarg_of_ipattern pat = in_gen (rawwit Tacarg.wit_intro_pattern) pat
 let genarg_of_uconstr c = in_gen (rawwit Stdarg.wit_uconstr) c
 let in_tac tac = in_gen (rawwit Tacarg.wit_ltac) tac
 
@@ -197,9 +198,9 @@ GEXTEND Gram
      non ambiguous name where dots are replaced by "_"? Probably too
      verbose most of the time. *)
   fresh_id:
-    [ [ s = STRING -> ArgArg s (*| id = ident -> ArgVar (!@loc,id)*)
+    [ [ s = STRING -> Locus.ArgArg s (*| id = ident -> Locus.ArgVar (!@loc,id)*)
         | qid = qualid -> let (_pth,id) = Libnames.repr_qualid qid.CAst.v in
-                          ArgVar (CAst.make ~loc:!@loc id) ] ]
+                          Locus.ArgVar (CAst.make ~loc:!@loc id) ] ]
   ;
   constr_eval:
     [ [ IDENT "eval"; rtc = red_expr; "in"; c = Constr.constr ->
diff --git a/plugins/ltac/g_rewrite.ml4 b/plugins/ltac/g_rewrite.ml4
index 079001ee40..2189e224ff 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 dc9f607cf0..05005c733a 100644
--- a/plugins/ltac/g_tactic.ml4
+++ b/plugins/ltac/g_tactic.ml4
@@ -11,12 +11,14 @@
 open Pp
 open CErrors
 open Util
+open Names
+open Namegen
 open Tacexpr
 open Genredexpr
 open Constrexpr
 open Libnames
 open Tok
-open Misctypes
+open Tactypes
 open Locus
 open Decl_kinds
 
@@ -383,19 +385,19 @@ GEXTEND Gram
   ;
   hypident:
     [ [ id = id_or_meta ->
-        let id : Misctypes.lident = id in
+        let id : lident = id in
         id,InHyp
       | "("; IDENT "type"; IDENT "of"; id = id_or_meta; ")" ->
-        let id : Misctypes.lident = id in
+        let id : lident = id in
         id,InHypTypeOnly
       | "("; IDENT "value"; IDENT "of"; id = id_or_meta; ")" ->
-        let id : Misctypes.lident = id in
+        let id : lident = id in
         id,InHypValueOnly
     ] ]
   ;
   hypident_occ:
     [ [ (id,l)=hypident; occs=occs ->
-        let id : Misctypes.lident = id in
+        let id : lident = id in
         ((occs,id),l) ] ]
   ;
   in_clause:
@@ -494,12 +496,12 @@ GEXTEND Gram
     | -> None ] ]
   ;
   rewriter :
-    [ [ "!"; c = constr_with_bindings_arg -> (RepeatPlus,c)
-      | ["?"| LEFTQMARK]; c = constr_with_bindings_arg -> (RepeatStar,c)
-      | n = natural; "!"; c = constr_with_bindings_arg -> (Precisely n,c)
-      |	n = natural; ["?" | LEFTQMARK]; c = constr_with_bindings_arg -> (UpTo n,c)
-      | n = natural; c = constr_with_bindings_arg -> (Precisely n,c)
-      | c = constr_with_bindings_arg -> (Precisely 1, c)
+    [ [ "!"; c = constr_with_bindings_arg -> (Equality.RepeatPlus,c)
+      | ["?"| LEFTQMARK]; c = constr_with_bindings_arg -> (Equality.RepeatStar,c)
+      | n = natural; "!"; c = constr_with_bindings_arg -> (Equality.Precisely n,c)
+      |	n = natural; ["?" | LEFTQMARK]; c = constr_with_bindings_arg -> (Equality.UpTo n,c)
+      | n = natural; c = constr_with_bindings_arg -> (Equality.Precisely n,c)
+      | c = constr_with_bindings_arg -> (Equality.Precisely 1, c)
       ] ]
   ;
   oriented_rewriter :
diff --git a/plugins/ltac/pltac.mli b/plugins/ltac/pltac.mli
index 434feba95c..4c075d4136 100644
--- a/plugins/ltac/pltac.mli
+++ b/plugins/ltac/pltac.mli
@@ -15,22 +15,22 @@ open Libnames
 open Constrexpr
 open Tacexpr
 open Genredexpr
-open Misctypes
+open Tactypes
 
 val open_constr : constr_expr Gram.entry
 val constr_with_bindings : constr_expr with_bindings Gram.entry
 val bindings : constr_expr bindings Gram.entry
-val hypident : (lident * Locus.hyp_location_flag) Gram.entry
+val hypident : (Names.lident * Locus.hyp_location_flag) Gram.entry
 val constr_may_eval : (constr_expr,reference or_by_notation,constr_expr) may_eval Gram.entry
 val constr_eval : (constr_expr,reference or_by_notation,constr_expr) may_eval Gram.entry
 val uconstr : constr_expr Gram.entry
 val quantified_hypothesis : quantified_hypothesis Gram.entry
 val destruction_arg : constr_expr with_bindings Tactics.destruction_arg Gram.entry
-val int_or_var : int or_var Gram.entry
+val int_or_var : int Locus.or_var Gram.entry
 val simple_tactic : raw_tactic_expr Gram.entry
 val simple_intropattern : constr_expr intro_pattern_expr CAst.t Gram.entry
-val in_clause : lident Locus.clause_expr Gram.entry
-val clause_dft_concl : lident Locus.clause_expr Gram.entry
+val in_clause : Names.lident Locus.clause_expr Gram.entry
+val clause_dft_concl : Names.lident Locus.clause_expr Gram.entry
 val tactic_arg : raw_tactic_arg Gram.entry
 val tactic_expr : raw_tactic_expr Gram.entry
 val binder_tactic : raw_tactic_expr Gram.entry
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index b29af6680d..e19a95e84d 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -19,7 +19,7 @@ open Geninterp
 open Stdarg
 open Libnames
 open Notation_gram
-open Misctypes
+open Tactypes
 open Locus
 open Decl_kinds
 open Genredexpr
@@ -493,7 +493,7 @@ let string_of_genarg_arg (ArgumentType arg) =
 
   let pr_orient b = if b then mt () else str "<- "
 
-  let pr_multi = function
+  let pr_multi = let open Equality in function
     | Precisely 1 -> mt ()
     | Precisely n -> int n ++ str "!"
     | UpTo n -> int n ++ str "?"
@@ -749,7 +749,7 @@ let pr_goal_selector ~toplevel s =
         | TacIntroPattern (ev,(_::_ as p)) ->
            hov 1 (primitive (if ev then "eintros" else "intros") ++
                     (match p with
-                    | [{CAst.v=Misctypes.IntroForthcoming false}] -> mt ()
+                    | [{CAst.v=IntroForthcoming false}] -> mt ()
                     | _ -> spc () ++ prlist_with_sep spc (Miscprint.pr_intro_pattern pr.pr_dconstr) p))
         | TacApply (a,ev,cb,inhyp) ->
           hov 1 (
diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli
index 5d2a996183..6c09e447a5 100644
--- a/plugins/ltac/pptactic.mli
+++ b/plugins/ltac/pptactic.mli
@@ -14,11 +14,11 @@
 open Genarg
 open Geninterp
 open Names
-open Misctypes
 open Environ
 open Constrexpr
 open Notation_gram
 open Tacexpr
+open Tactypes
 
 type 'a grammar_tactic_prod_item_expr =
 | TacTerm of string
@@ -97,7 +97,7 @@ val pr_may_eval :
   ('a -> Pp.t) -> ('a -> Pp.t) -> ('b -> Pp.t) ->
   ('c -> Pp.t) -> ('a,'b,'c) Genredexpr.may_eval -> Pp.t
 
-val pr_and_short_name : ('a -> Pp.t) -> 'a and_short_name -> Pp.t
+val pr_and_short_name : ('a -> Pp.t) -> 'a Stdarg.and_short_name -> Pp.t
 val pr_or_by_notation : ('a -> Pp.t) -> 'a or_by_notation -> Pp.t
 
 val pr_evaluable_reference_env : env -> evaluable_global_reference -> Pp.t
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index b91315aca7..cd04f4ae9a 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 1e3d4733b5..0d014a0bf3 100644
--- a/plugins/ltac/rewrite.mli
+++ b/plugins/ltac/rewrite.mli
@@ -12,9 +12,9 @@ open Names
 open Environ
 open EConstr
 open Constrexpr
-open Tacexpr
-open Misctypes
 open Evd
+open Tactypes
+open Tacexpr
 open Tacinterp
 
 (** TODO: document and clean me! *)
diff --git a/plugins/ltac/tacarg.ml b/plugins/ltac/tacarg.ml
index 6eb482b1c3..8a25d4851f 100644
--- a/plugins/ltac/tacarg.ml
+++ b/plugins/ltac/tacarg.ml
@@ -19,6 +19,14 @@ let make0 ?dyn name =
   let () = Geninterp.register_val0 wit dyn in
   wit
 
+let wit_intro_pattern = make0 "intropattern"
+let wit_quant_hyp = make0 "quant_hyp"
+let wit_constr_with_bindings = make0 "constr_with_bindings"
+let wit_open_constr_with_bindings = make0 "open_constr_with_bindings"
+let wit_bindings = make0 "bindings"
+let wit_quantified_hypothesis = wit_quant_hyp
+let wit_intropattern = wit_intro_pattern
+
 let wit_tactic : (raw_tactic_expr, glob_tactic_expr, Val.t) genarg_type =
   make0 "tactic"
 
diff --git a/plugins/ltac/tacarg.mli b/plugins/ltac/tacarg.mli
index 59473a5e57..bdb0be03cf 100644
--- a/plugins/ltac/tacarg.mli
+++ b/plugins/ltac/tacarg.mli
@@ -9,9 +9,33 @@
 (************************************************************************)
 
 open Genarg
-open Tacexpr
+open EConstr
 open Constrexpr
-open Misctypes
+open Tactypes
+open Tacexpr
+
+(** Tactic related witnesses, could also live in tactics/ if other users *)
+val wit_intro_pattern : (constr_expr intro_pattern_expr CAst.t, glob_constr_and_expr intro_pattern_expr CAst.t, intro_pattern) genarg_type
+
+val wit_quant_hyp : quantified_hypothesis uniform_genarg_type
+
+val wit_constr_with_bindings :
+  (constr_expr with_bindings,
+  glob_constr_and_expr with_bindings,
+  constr with_bindings delayed_open) genarg_type
+
+val wit_open_constr_with_bindings :
+  (constr_expr with_bindings,
+  glob_constr_and_expr with_bindings,
+  constr with_bindings delayed_open) genarg_type
+
+val wit_bindings :
+  (constr_expr bindings,
+  glob_constr_and_expr bindings,
+  constr bindings delayed_open) genarg_type
+
+val wit_quantified_hypothesis : quantified_hypothesis uniform_genarg_type
+val wit_intropattern : (constr_expr intro_pattern_expr CAst.t, glob_constr_and_expr intro_pattern_expr CAst.t, intro_pattern) genarg_type
 
 (** Generic arguments based on Ltac. *)
 
diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml
index 3812a2ba29..cc9c2046d8 100644
--- a/plugins/ltac/taccoerce.ml
+++ b/plugins/ltac/taccoerce.ml
@@ -12,9 +12,11 @@ open Util
 open Names
 open Constr
 open EConstr
-open Misctypes
+open Namegen
+open Tactypes
 open Genarg
 open Stdarg
+open Tacarg
 open Geninterp
 open Pp
 
@@ -365,7 +367,7 @@ let coerce_to_int_or_var_list v =
   match Value.to_list v with
   | None -> raise (CannotCoerceTo "an int list")
   | Some l ->
-    let map n = ArgArg (coerce_to_int n) in
+    let map n = Locus.ArgArg (coerce_to_int n) in
     List.map map l
 
 (** Abstract application, to print ltac functions *)
diff --git a/plugins/ltac/taccoerce.mli b/plugins/ltac/taccoerce.mli
index 5185217cda..56f8816840 100644
--- a/plugins/ltac/taccoerce.mli
+++ b/plugins/ltac/taccoerce.mli
@@ -11,9 +11,9 @@
 open Util
 open Names
 open EConstr
-open Misctypes
 open Genarg
 open Geninterp
+open Tactypes
 
 (** Coercions from highest level generic arguments to actual data used by Ltac
     interpretation. Those functions examinate dynamic types and try to return
@@ -56,7 +56,7 @@ val coerce_to_ident_not_fresh : Environ.env -> Evd.evar_map -> Value.t -> Id.t
 val coerce_to_intro_pattern : Environ.env -> Evd.evar_map -> Value.t -> Tacexpr.delayed_open_constr intro_pattern_expr
 
 val coerce_to_intro_pattern_naming :
-  Environ.env -> Evd.evar_map -> Value.t -> intro_pattern_naming_expr
+  Environ.env -> Evd.evar_map -> Value.t -> Namegen.intro_pattern_naming_expr
 
 val coerce_to_hint_base : Value.t -> string
 
@@ -86,7 +86,7 @@ val coerce_to_quantified_hypothesis : Evd.evar_map -> Value.t -> quantified_hypo
 
 val coerce_to_decl_or_quant_hyp : Environ.env -> Evd.evar_map -> Value.t -> quantified_hypothesis
 
-val coerce_to_int_or_var_list : Value.t -> int or_var list
+val coerce_to_int_or_var_list : Value.t -> int Locus.or_var list
 
 (** {5 Missing generic arguments} *)
 
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index e510b9f591..fada7424c3 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -376,7 +376,7 @@ let add_ml_tactic_notation name ~level prods =
     in
     let ids = List.map_filter get_id prods in
     let entry = { mltac_name = name; mltac_index = len - i - 1 } in
-    let map id = Reference (Misctypes.ArgVar (CAst.make id)) in
+    let map id = Reference (Locus.ArgVar (CAst.make id)) in
     let tac = TacML (Loc.tag (entry, List.map map ids)) in
     add_glob_tactic_notation false ~level prods true ids tac
   in
diff --git a/plugins/ltac/tacexpr.ml b/plugins/ltac/tacexpr.ml
index 17f5e5d41a..d51de8c650 100644
--- a/plugins/ltac/tacexpr.ml
+++ b/plugins/ltac/tacexpr.ml
@@ -15,7 +15,7 @@ open Libnames
 open Genredexpr
 open Genarg
 open Pattern
-open Misctypes
+open Tactypes
 open Locus
 
 type ltac_constant = KerName.t
@@ -75,7 +75,7 @@ type 'id message_token =
 
 type ('dconstr,'id) induction_clause =
     'dconstr with_bindings Tactics.destruction_arg *
-    (intro_pattern_naming_expr CAst.t option (* eqn:... *)
+    (Namegen.intro_pattern_naming_expr CAst.t option (* eqn:... *)
     * 'dconstr or_and_intro_pattern_expr CAst.t or_var option) (* as ... *)
     * 'id clause_expr option (* in ... *)
 
@@ -117,7 +117,7 @@ type ml_tactic_entry = {
 
 (** Composite types *)
 
-type glob_constr_and_expr = Tactypes.glob_constr_and_expr
+type glob_constr_and_expr = Genintern.glob_constr_and_expr
 
 type open_constr_expr = unit * constr_expr
 type open_glob_constr = unit * glob_constr_and_expr
@@ -134,7 +134,7 @@ type delayed_open_constr = EConstr.constr delayed_open
 type intro_pattern = delayed_open_constr intro_pattern_expr CAst.t
 type intro_patterns = delayed_open_constr intro_pattern_expr CAst.t list
 type or_and_intro_pattern = delayed_open_constr or_and_intro_pattern_expr CAst.t
-type intro_pattern_naming = intro_pattern_naming_expr CAst.t
+type intro_pattern_naming = Namegen.intro_pattern_naming_expr CAst.t
 
 (** Generic expressions for atomic tactics *)
 
@@ -152,7 +152,7 @@ type 'a gen_atomic_tactic_expr =
       'dtrm intro_pattern_expr CAst.t option * 'trm
   | TacGeneralize of ('trm with_occurrences * Name.t) list
   | TacLetTac of evars_flag * Name.t * 'trm * 'nam clause_expr * letin_flag *
-      intro_pattern_naming_expr CAst.t option
+      Namegen.intro_pattern_naming_expr CAst.t option
 
   (* Derived basic tactics *)
   | TacInductionDestruct of
@@ -164,7 +164,7 @@ type 'a gen_atomic_tactic_expr =
 
   (* Equality and inversion *)
   | TacRewrite of evars_flag *
-      (bool * multi * 'dtrm with_bindings_arg) list * 'nam clause_expr *
+      (bool * Equality.multi * 'dtrm with_bindings_arg) list * 'nam clause_expr *
       (* spiwack: using ['dtrm] here is a small hack, may not be
          stable by a change in the representation of delayed
          terms. Because, in fact, it is the whole "with_bindings"
@@ -305,7 +305,7 @@ constraint 'a = <
 
 type g_trm = glob_constr_and_expr
 type g_pat = glob_constr_pattern_and_expr
-type g_cst = evaluable_global_reference and_short_name or_var
+type g_cst = evaluable_global_reference Stdarg.and_short_name or_var
 type g_ref = ltac_constant located or_var
 type g_nam = lident
 
diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli
index 17f5e5d41a..01eead164b 100644
--- a/plugins/ltac/tacexpr.mli
+++ b/plugins/ltac/tacexpr.mli
@@ -15,8 +15,8 @@ open Libnames
 open Genredexpr
 open Genarg
 open Pattern
-open Misctypes
 open Locus
+open Tactypes
 
 type ltac_constant = KerName.t
 
@@ -75,7 +75,7 @@ type 'id message_token =
 
 type ('dconstr,'id) induction_clause =
     'dconstr with_bindings Tactics.destruction_arg *
-    (intro_pattern_naming_expr CAst.t option (* eqn:... *)
+    (Namegen.intro_pattern_naming_expr CAst.t option (* eqn:... *)
     * 'dconstr or_and_intro_pattern_expr CAst.t or_var option) (* as ... *)
     * 'id clause_expr option (* in ... *)
 
@@ -117,7 +117,7 @@ type ml_tactic_entry = {
 
 (** Composite types *)
 
-type glob_constr_and_expr = Tactypes.glob_constr_and_expr
+type glob_constr_and_expr = Genintern.glob_constr_and_expr
 
 type open_constr_expr = unit * constr_expr
 type open_glob_constr = unit * glob_constr_and_expr
@@ -134,7 +134,7 @@ type delayed_open_constr = EConstr.constr delayed_open
 type intro_pattern = delayed_open_constr intro_pattern_expr CAst.t
 type intro_patterns = delayed_open_constr intro_pattern_expr CAst.t list
 type or_and_intro_pattern = delayed_open_constr or_and_intro_pattern_expr CAst.t
-type intro_pattern_naming = intro_pattern_naming_expr CAst.t
+type intro_pattern_naming = Namegen.intro_pattern_naming_expr CAst.t
 
 (** Generic expressions for atomic tactics *)
 
@@ -152,7 +152,7 @@ type 'a gen_atomic_tactic_expr =
       'dtrm intro_pattern_expr CAst.t option * 'trm
   | TacGeneralize of ('trm with_occurrences * Name.t) list
   | TacLetTac of evars_flag * Name.t * 'trm * 'nam clause_expr * letin_flag *
-      intro_pattern_naming_expr CAst.t option
+      Namegen.intro_pattern_naming_expr CAst.t option
 
   (* Derived basic tactics *)
   | TacInductionDestruct of
@@ -164,7 +164,7 @@ type 'a gen_atomic_tactic_expr =
 
   (* Equality and inversion *)
   | TacRewrite of evars_flag *
-      (bool * multi * 'dtrm with_bindings_arg) list * 'nam clause_expr *
+      (bool * Equality.multi * 'dtrm with_bindings_arg) list * 'nam clause_expr *
       (* spiwack: using ['dtrm] here is a small hack, may not be
          stable by a change in the representation of delayed
          terms. Because, in fact, it is the whole "with_bindings"
@@ -305,7 +305,7 @@ constraint 'a = <
 
 type g_trm = glob_constr_and_expr
 type g_pat = glob_constr_pattern_and_expr
-type g_cst = evaluable_global_reference and_short_name or_var
+type g_cst = evaluable_global_reference Stdarg.and_short_name or_var
 type g_ref = ltac_constant located or_var
 type g_nam = lident
 
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index 9ad9e1520e..cef5bb1b8e 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -27,7 +27,8 @@ open Tacexpr
 open Genarg
 open Stdarg
 open Tacarg
-open Misctypes
+open Namegen
+open Tactypes
 open Locus
 
 (** Globalization of tactic expressions :
diff --git a/plugins/ltac/tacintern.mli b/plugins/ltac/tacintern.mli
index fb32508cc9..9146fced2d 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 a93cf5ae7c..8a8f9e71aa 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -12,6 +12,7 @@ open Constrintern
 open Patternops
 open Pp
 open CAst
+open Namegen
 open Genredexpr
 open Glob_term
 open Glob_ops
@@ -35,7 +36,7 @@ open Stdarg
 open Tacarg
 open Printer
 open Pretyping
-open Misctypes
+open Tactypes
 open Locus
 open Tacintern
 open Taccoerce
diff --git a/plugins/ltac/tacinterp.mli b/plugins/ltac/tacinterp.mli
index bd44bdbea4..fd2d96bd62 100644
--- a/plugins/ltac/tacinterp.mli
+++ b/plugins/ltac/tacinterp.mli
@@ -14,7 +14,7 @@ open EConstr
 open Tacexpr
 open Genarg
 open Redexpr
-open Misctypes
+open Tactypes
 
 val ltac_trace_info : ltac_trace Exninfo.t
 
@@ -131,7 +131,7 @@ val interp_ltac_var : (value -> 'a) -> interp_sign ->
 
 val interp_int : interp_sign -> lident -> int
 
-val interp_int_or_var : interp_sign -> int or_var -> int
+val interp_int_or_var : interp_sign -> int Locus.or_var -> int
 
 val default_ist : unit -> Geninterp.interp_sign
 (** Empty ist with debug set on the current value. *)
diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml
index 50bf687b1d..dd799dc131 100644
--- a/plugins/ltac/tacsubst.ml
+++ b/plugins/ltac/tacsubst.ml
@@ -14,7 +14,7 @@ open Mod_subst
 open Genarg
 open Stdarg
 open Tacarg
-open Misctypes
+open Tactypes
 open Globnames
 open Genredexpr
 open Patternops
@@ -75,7 +75,7 @@ let subst_and_short_name f (c,n) =
 (*  assert (n=None); *)(* since tacdef are strictly globalized *)
   (f c,None)
 
-let subst_or_var f =  function
+let subst_or_var f =  let open Locus in function
   | ArgVar _ as x -> x
   | ArgArg x -> ArgArg (f x)
 
diff --git a/plugins/ltac/tacsubst.mli b/plugins/ltac/tacsubst.mli
index 0a894791b0..d406686c56 100644
--- a/plugins/ltac/tacsubst.mli
+++ b/plugins/ltac/tacsubst.mli
@@ -11,7 +11,7 @@
 open Tacexpr
 open Mod_subst
 open Genarg
-open Misctypes
+open Tactypes
 
 (** Substitution of tactics at module closing time *)
 
diff --git a/plugins/ltac/tactic_debug.mli b/plugins/ltac/tactic_debug.mli
index 734e76b563..175341df09 100644
--- a/plugins/ltac/tactic_debug.mli
+++ b/plugins/ltac/tactic_debug.mli
@@ -76,7 +76,7 @@ val db_logic_failure : debug_info -> exn -> unit Proofview.NonLogical.t
 
 (** Prints a logic failure message for a rule *)
 val db_breakpoint : debug_info ->
-  Misctypes.lident message_token list -> unit Proofview.NonLogical.t
+  lident message_token list -> unit Proofview.NonLogical.t
 
 val extract_ltac_trace :
   ?loc:Loc.t -> Tacexpr.ltac_trace -> Pp.t option Loc.located
diff --git a/plugins/ltac/tauto.ml b/plugins/ltac/tauto.ml
index 8eeb8903e7..299bc7ea4d 100644
--- a/plugins/ltac/tauto.ml
+++ b/plugins/ltac/tauto.ml
@@ -13,7 +13,6 @@ open EConstr
 open Hipattern
 open Names
 open Geninterp
-open Misctypes
 open Ltac_plugin
 open Tacexpr
 open Tacinterp
@@ -94,7 +93,7 @@ let clear id = Tactics.clear [id]
 
 let assumption = Tactics.assumption
 
-let split = Tactics.split_with_bindings false [Misctypes.NoBindings]
+let split = Tactics.split_with_bindings false [Tactypes.NoBindings]
 
 (** Test *)
 
@@ -175,7 +174,7 @@ let flatten_contravariant_disj _ ist =
   | Some (_,args) ->
       let map i arg =
         let typ = mkArrow arg c in
-        let ci = Tactics.constructor_tac false None (succ i) Misctypes.NoBindings in
+        let ci = Tactics.constructor_tac false None (succ i) Tactypes.NoBindings in
         let by = tclTHENLIST [intro; apply hyp; ci; assumption] in
         assert_ ~by typ
       in
@@ -187,7 +186,7 @@ let flatten_contravariant_disj _ ist =
 let make_unfold name =
   let dir = DirPath.make (List.map Id.of_string ["Logic"; "Init"; "Coq"]) in
   let const = Constant.make2 (ModPath.MPfile dir) (Label.make name) in
-  (Locus.AllOccurrences, ArgArg (EvalConstRef const, None))
+  Locus.(AllOccurrences, ArgArg (EvalConstRef const, None))
 
 let u_not = make_unfold "not"
 
@@ -245,7 +244,7 @@ let with_flags flags _ ist =
   let x = CAst.make @@ Id.of_string "x" in
   let arg = Val.Dyn (tag_tauto_flags, flags) in
   let ist = { ist with lfun = Id.Map.add x.CAst.v arg ist.lfun } in
-  eval_tactic_ist ist (TacArg (Loc.tag @@ TacCall (Loc.tag (ArgVar f, [Reference (ArgVar x)]))))
+  eval_tactic_ist ist (TacArg (Loc.tag @@ TacCall (Loc.tag (Locus.ArgVar f, [Reference (Locus.ArgVar x)]))))
 
 let register_tauto_tactic tac name0 args =
   let ids = List.map (fun id -> Id.of_string id) args in