25 files changed, 114 insertions, 69 deletions
diff --git a/interp/constrarg.ml b/interp/constrarg.ml
index aaf33a956..b8baa6401 100644
--- a/interp/constrarg.ml
+++ b/interp/constrarg.ml
@@ -8,6 +8,7 @@
 
 open Loc
 open Misctypes
+open Tactypes
 open Genarg
 open Geninterp
 
@@ -26,7 +27,7 @@ let loc_of_or_by_notation f = function
 let wit_int_or_var =
   make0 ~dyn:(val_tag (topwit Stdarg.wit_int)) "int_or_var"
 
-let wit_intro_pattern : (Constrexpr.constr_expr intro_pattern_expr located, Tacexpr.glob_constr_and_expr intro_pattern_expr located, Tacexpr.intro_pattern) genarg_type =
+let wit_intro_pattern : (Constrexpr.constr_expr intro_pattern_expr located, glob_constr_and_expr intro_pattern_expr located, intro_pattern) genarg_type =
   make0 "intropattern"
 
 let wit_ident =
diff --git a/interp/constrarg.mli b/interp/constrarg.mli
index 32f2dc6f3..4b542675b 100644
--- a/interp/constrarg.mli
+++ b/interp/constrarg.mli
@@ -18,6 +18,7 @@ open Genredexpr
 open Pattern
 open Constrexpr
 open Misctypes
+open Tactypes
 open Genarg
 
 (** FIXME: nothing to do there. *)
@@ -27,7 +28,7 @@ val loc_of_or_by_notation : ('a -> Loc.t) -> 'a or_by_notation -> Loc.t
 
 val wit_int_or_var : (int or_var, int or_var, int) genarg_type
 
-val wit_intro_pattern : (constr_expr intro_pattern_expr located, Tacexpr.glob_constr_and_expr intro_pattern_expr located, Tacexpr.intro_pattern) genarg_type
+val wit_intro_pattern : (constr_expr intro_pattern_expr located, glob_constr_and_expr intro_pattern_expr located, intro_pattern) genarg_type
 
 val wit_ident : Id.t uniform_genarg_type
 
@@ -37,26 +38,26 @@ val wit_ref : (reference, global_reference located or_var, global_reference) gen
 
 val wit_quant_hyp : quantified_hypothesis uniform_genarg_type
 
-val wit_constr : (constr_expr, Tacexpr.glob_constr_and_expr, constr) genarg_type
+val wit_constr : (constr_expr, glob_constr_and_expr, constr) genarg_type
 
-val wit_uconstr : (constr_expr , Tacexpr.glob_constr_and_expr, Glob_term.closed_glob_constr) genarg_type
+val wit_uconstr : (constr_expr , glob_constr_and_expr, Glob_term.closed_glob_constr) genarg_type
 
 val wit_open_constr :
-  (constr_expr, Tacexpr.glob_constr_and_expr, constr) genarg_type
+  (constr_expr, glob_constr_and_expr, constr) genarg_type
 
 val wit_constr_with_bindings :
   (constr_expr with_bindings,
-  Tacexpr.glob_constr_and_expr with_bindings,
-  constr with_bindings Pretyping.delayed_open) genarg_type
+  glob_constr_and_expr with_bindings,
+  constr with_bindings delayed_open) genarg_type
 
 val wit_bindings :
   (constr_expr bindings,
-  Tacexpr.glob_constr_and_expr bindings,
-  constr bindings Pretyping.delayed_open) genarg_type
+  glob_constr_and_expr bindings,
+  constr bindings delayed_open) genarg_type
 
 val wit_red_expr :
   ((constr_expr,reference or_by_notation,constr_expr) red_expr_gen,
-  (Tacexpr.glob_constr_and_expr,evaluable_global_reference and_short_name or_var,Tacexpr.glob_constr_pattern_and_expr) red_expr_gen,
+  (glob_constr_and_expr,evaluable_global_reference and_short_name or_var,glob_constr_pattern_and_expr) red_expr_gen,
   (constr,evaluable_global_reference,constr_pattern) red_expr_gen) genarg_type
 
 val wit_clause_dft_concl :  (Names.Id.t Loc.located Locus.clause_expr,Names.Id.t Loc.located Locus.clause_expr,Names.Id.t Locus.clause_expr) genarg_type
@@ -67,8 +68,8 @@ val wit_reference : (reference, global_reference located or_var, global_referenc
 val wit_global : (reference, global_reference located or_var, global_reference) genarg_type
 val wit_clause :  (Names.Id.t Loc.located Locus.clause_expr,Names.Id.t Loc.located Locus.clause_expr,Names.Id.t Locus.clause_expr) genarg_type
 val wit_quantified_hypothesis : quantified_hypothesis uniform_genarg_type
-val wit_intropattern : (constr_expr intro_pattern_expr located, Tacexpr.glob_constr_and_expr intro_pattern_expr located, Tacexpr.intro_pattern) genarg_type
+val wit_intropattern : (constr_expr intro_pattern_expr located, glob_constr_and_expr intro_pattern_expr located, intro_pattern) genarg_type
 val wit_redexpr :
   ((constr_expr,reference or_by_notation,constr_expr) red_expr_gen,
-  (Tacexpr.glob_constr_and_expr,evaluable_global_reference and_short_name or_var,Tacexpr.glob_constr_pattern_and_expr) red_expr_gen,
+  (glob_constr_and_expr,evaluable_global_reference and_short_name or_var,glob_constr_pattern_and_expr) red_expr_gen,
   (constr,evaluable_global_reference,constr_pattern) red_expr_gen) genarg_type
diff --git a/interp/genintern.ml b/interp/genintern.ml
index 693101a47..be7abfa99 100644
--- a/interp/genintern.ml
+++ b/interp/genintern.ml
@@ -16,7 +16,7 @@ type glob_sign = {
 
 type ('raw, 'glb) intern_fun = glob_sign -> 'raw -> glob_sign * 'glb
 type 'glb subst_fun = substitution -> 'glb -> 'glb
-type 'glb ntn_subst_fun = Tacexpr.glob_constr_and_expr Id.Map.t -> 'glb -> 'glb
+type 'glb ntn_subst_fun = Tactypes.glob_constr_and_expr Id.Map.t -> 'glb -> 'glb
 
 module InternObj =
 struct
diff --git a/interp/genintern.mli b/interp/genintern.mli
index aabb85e00..4b0354be3 100644
--- a/interp/genintern.mli
+++ b/interp/genintern.mli
@@ -34,7 +34,7 @@ val generic_substitute : glob_generic_argument subst_fun
 
 (** {5 Notation functions} *)
 
-type 'glb ntn_subst_fun = Tacexpr.glob_constr_and_expr Id.Map.t -> 'glb -> 'glb
+type 'glb ntn_subst_fun = Tactypes.glob_constr_and_expr Id.Map.t -> 'glb -> 'glb
 
 val substitute_notation : ('raw, 'glb, 'top) genarg_type -> 'glb ntn_subst_fun
 
diff --git a/intf/misctypes.mli b/intf/misctypes.mli
index c6c4b01e4..e4f595ac4 100644
--- a/intf/misctypes.mli
+++ b/intf/misctypes.mli
@@ -117,3 +117,22 @@ type rec_flag = bool       (* true = recursive        false = not recursive *)
 type advanced_flag = bool  (* true = advanced         false = basic *)
 type letin_flag = bool     (* true = use local def    false = use Leibniz *)
 type clear_flag = bool option (* true = clear hyp, false = keep hyp, None = use default *)
+
+type multi =
+  | Precisely of int
+  | UpTo of int
+  | RepeatStar
+  | RepeatPlus
+
+type 'a core_destruction_arg =
+  | ElimOnConstr of 'a
+  | ElimOnIdent of Id.t Loc.located
+  | ElimOnAnonHyp of int
+
+type 'a destruction_arg =
+  clear_flag * 'a core_destruction_arg
+
+type inversion_kind =
+  | SimpleInversion
+  | FullInversion
+  | FullInversionClear
diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index cf33d7973..9c25a1645 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -32,15 +32,13 @@ type advanced_flag = bool  (* true = advanced         false = basic *)
 type letin_flag = bool     (* true = use local def    false = use Leibniz *)
 type clear_flag = bool option (* true = clear hyp, false = keep hyp, None = use default *)
 
-type debug = Debug | Info | Off (* for trivial / auto / eauto ... *)
-
 type goal_selector = Vernacexpr.goal_selector =
   | SelectNth of int
   | SelectList of (int * int) list
   | SelectId of Id.t
   | SelectAll
 
-type 'a core_destruction_arg =
+type 'a core_destruction_arg = 'a Misctypes.core_destruction_arg =
   | ElimOnConstr of 'a
   | ElimOnIdent of Id.t located
   | ElimOnAnonHyp of int
@@ -48,7 +46,7 @@ type 'a core_destruction_arg =
 type 'a destruction_arg =
   clear_flag * 'a core_destruction_arg
 
-type inversion_kind =
+type inversion_kind = Misctypes.inversion_kind =
   | SimpleInversion
   | FullInversion
   | FullInversionClear
@@ -79,12 +77,6 @@ type ('constr,'dconstr,'id) induction_clause_list =
 
 type 'a with_bindings_arg = clear_flag * 'a with_bindings
 
-type multi =
-  | Precisely of int
-  | UpTo of int
-  | RepeatStar
-  | RepeatPlus
-
 (* Type of patterns *)
 type 'a match_pattern =
   | Term of 'a
@@ -117,10 +109,7 @@ type ml_tactic_entry = {
 
 (** Composite types *)
 
-(** In globalize tactics, we need to keep the initial [constr_expr] to recompute
-   in the environment by the effective calls to Intro, Inversion, etc 
-   The [constr_expr] field is [None] in TacDef though *)
-type glob_constr_and_expr = Glob_term.glob_constr * constr_expr option
+type glob_constr_and_expr = Tactypes.glob_constr_and_expr
 
 type open_constr_expr = unit * constr_expr
 type open_glob_constr = unit * glob_constr_and_expr
@@ -128,7 +117,7 @@ type open_glob_constr = unit * glob_constr_and_expr
 type binding_bound_vars = Constr_matching.binding_bound_vars
 type glob_constr_pattern_and_expr = binding_bound_vars * glob_constr_and_expr * constr_pattern
 
-type 'a delayed_open = 'a Pretyping.delayed_open =
+type 'a delayed_open = 'a Tactypes.delayed_open =
   { delayed : 'r. Environ.env -> 'r Sigma.t -> ('a, 'r) Sigma.sigma }
 
 type delayed_open_constr_with_bindings = Term.constr with_bindings delayed_open
diff --git a/intf/tactypes.mli b/intf/tactypes.mli
new file mode 100644
index 000000000..b96cb67df
--- /dev/null
+++ b/intf/tactypes.mli
@@ -0,0 +1,35 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(** Tactic-related types that are not totally Ltac specific and still used in
+    lower API. It's not clear whether this is a temporary API or if this is
+    meant to stay. *)
+
+open Loc
+open Names
+open Constrexpr
+open Glob_term
+open Pattern
+open Misctypes
+
+(** In globalize tactics, we need to keep the initial [constr_expr] to recompute
+   in the environment by the effective calls to Intro, Inversion, etc 
+   The [constr_expr] field is [None] in TacDef though *)
+type glob_constr_and_expr = Glob_term.glob_constr * constr_expr option
+type glob_constr_pattern_and_expr = Id.Set.t * glob_constr_and_expr * constr_pattern
+
+type 'a delayed_open =
+  { delayed : 'r. Environ.env -> 'r Sigma.t -> ('a, 'r) Sigma.sigma }
+
+type delayed_open_constr = Term.constr delayed_open
+type delayed_open_constr_with_bindings = Term.constr with_bindings delayed_open
+
+type intro_pattern = delayed_open_constr intro_pattern_expr located
+type intro_patterns = delayed_open_constr intro_pattern_expr located list
+type or_and_intro_pattern = delayed_open_constr or_and_intro_pattern_expr located
+type intro_pattern_naming = intro_pattern_naming_expr located
diff --git a/ltac/g_auto.ml4 b/ltac/g_auto.ml4
index eb1dc9081..2165e826e 100644
--- a/ltac/g_auto.ml4
+++ b/ltac/g_auto.ml4
@@ -15,6 +15,7 @@ open Constrarg
 open Pcoq.Prim
 open Pcoq.Constr
 open Pltac
+open Hints
 open Tacexpr
 
 DECLARE PLUGIN "g_auto"
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 0d9bde2ec..7d79de268 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -43,6 +43,7 @@ open Glob_ops
 open Evarconv
 open Pattern
 open Misctypes
+open Tactypes
 open Sigma.Notations
 
 module NamedDecl = Context.Named.Declaration
@@ -59,9 +60,6 @@ type ltac_var_map = {
 }
 type glob_constr_ltac_closure = ltac_var_map * glob_constr
 type pure_open_constr = evar_map * constr
-type 'a delayed_open =
-  { delayed : 'r. Environ.env -> 'r Sigma.t -> ('a, 'r) Sigma.sigma }
-type delayed_open_constr = constr delayed_open
 
 (************************************************************************)
 (* This concerns Cases *)
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 7cb256e4f..f015813af 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -55,11 +55,6 @@ type inference_flags = {
   expand_evars : bool
 }
 
-type 'a delayed_open =
-  { delayed : 'r. Environ.env -> 'r Sigma.t -> ('a, 'r) Sigma.sigma }
-
-type delayed_open_constr = constr delayed_open
-
 val default_inference_flags : bool -> inference_flags
 
 val no_classes_no_fail_inference_flags : inference_flags
@@ -122,7 +117,7 @@ val understand_judgment_tcc : env -> evar_map ref ->
 val type_uconstr :
   ?flags:inference_flags ->
   ?expected_type:typing_constraint ->
-  Geninterp.interp_sign -> Glob_term.closed_glob_constr -> constr delayed_open
+  Geninterp.interp_sign -> Glob_term.closed_glob_constr -> constr Tactypes.delayed_open
 
 (** Trying to solve remaining evars and remaining conversion problems
     possibly using type classes, heuristics, external tactic solver
diff --git a/tactics/auto.mli b/tactics/auto.mli
index f68190498..1689bd73c 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -14,6 +14,7 @@ open Clenv
 open Pattern
 open Decl_kinds
 open Hints
+open Tactypes
 
 val priority : ('a * full_hint) list -> ('a * full_hint) list
 
@@ -40,24 +41,24 @@ val conclPattern : constr -> constr_pattern option -> Genarg.glob_generic_argume
     "nocore" amongst the databases. *)
 
 val auto : ?debug:debug ->
-  int -> Pretyping.delayed_open_constr list -> hint_db_name list -> unit Proofview.tactic
+  int -> delayed_open_constr list -> hint_db_name list -> unit Proofview.tactic
 
 (** Auto with more delta. *)
 
 val new_auto : ?debug:debug ->
-  int -> Pretyping.delayed_open_constr list -> hint_db_name list -> unit Proofview.tactic
+  int -> delayed_open_constr list -> hint_db_name list -> unit Proofview.tactic
 
 (** auto with default search depth and with the hint database "core" *)
 val default_auto : unit Proofview.tactic
 
 (** auto with all hint databases except the "v62" compatibility database *)
 val full_auto : ?debug:debug ->
-  int -> Pretyping.delayed_open_constr list -> unit Proofview.tactic
+  int -> delayed_open_constr list -> unit Proofview.tactic
 
 (** auto with all hint databases except the "v62" compatibility database
    and doing delta *)
 val new_full_auto : ?debug:debug ->
-  int -> Pretyping.delayed_open_constr list -> unit Proofview.tactic
+  int -> delayed_open_constr list -> unit Proofview.tactic
 
 (** auto with default search depth and with all hint databases
    except the "v62" compatibility database *)
@@ -65,19 +66,19 @@ val default_full_auto : unit Proofview.tactic
 
 (** The generic form of auto (second arg [None] means all bases) *)
 val gen_auto : ?debug:debug ->
-  int option -> Pretyping.delayed_open_constr list -> hint_db_name list option -> unit Proofview.tactic
+  int option -> delayed_open_constr list -> hint_db_name list option -> unit Proofview.tactic
 
 (** The hidden version of auto *)
 val h_auto   : ?debug:debug ->
-  int option -> Pretyping.delayed_open_constr list -> hint_db_name list option -> unit Proofview.tactic
+  int option -> delayed_open_constr list -> hint_db_name list option -> unit Proofview.tactic
 
 (** Trivial *)
 
 val trivial : ?debug:debug ->
-  Pretyping.delayed_open_constr list -> hint_db_name list -> unit Proofview.tactic
+  delayed_open_constr list -> hint_db_name list -> unit Proofview.tactic
 val gen_trivial : ?debug:debug ->
-  Pretyping.delayed_open_constr list -> hint_db_name list option -> unit Proofview.tactic
+  delayed_open_constr list -> hint_db_name list option -> unit Proofview.tactic
 val full_trivial : ?debug:debug ->
-  Pretyping.delayed_open_constr list -> unit Proofview.tactic
+  delayed_open_constr list -> unit Proofview.tactic
 val h_trivial : ?debug:debug ->
-  Pretyping.delayed_open_constr list -> hint_db_name list option -> unit Proofview.tactic
+  delayed_open_constr list -> hint_db_name list option -> unit Proofview.tactic
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index 5ed8e439e..bac4d27c3 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -20,6 +20,7 @@ open Tactics
 open Clenv
 open Auto
 open Genredexpr
+open Tactypes
 open Locus
 open Locusops
 open Hints
@@ -202,7 +203,7 @@ type search_state = {
   dblist : hint_db list;
   localdb :  hint_db list;
   prev : prev_search_state;
-  local_lemmas : Pretyping.delayed_open_constr list;
+  local_lemmas : delayed_open_constr list;
 }
 
 and prev_search_state = (* for info eauto *)
diff --git a/tactics/eauto.mli b/tactics/eauto.mli
index 500717817..1f69e4ab3 100644
--- a/tactics/eauto.mli
+++ b/tactics/eauto.mli
@@ -9,6 +9,7 @@
 open Term
 open Proof_type
 open Hints
+open Tactypes
 
 val e_assumption : unit Proofview.tactic
 
@@ -16,15 +17,15 @@ val registered_e_assumption : unit Proofview.tactic
 
 val e_give_exact : ?flags:Unification.unify_flags -> constr -> unit Proofview.tactic
 
-val prolog_tac : Pretyping.delayed_open_constr list -> int -> unit Proofview.tactic
+val prolog_tac : delayed_open_constr list -> int -> unit Proofview.tactic
 
-val gen_eauto : ?debug:debug -> bool * int -> Pretyping.delayed_open_constr list ->
+val gen_eauto : ?debug:debug -> bool * int -> delayed_open_constr list ->
   hint_db_name list option -> unit Proofview.tactic
 
 val eauto_with_bases :
   ?debug:debug ->
   bool * int ->
-  Pretyping.delayed_open_constr list -> hint_db list -> Proof_type.tactic
+  delayed_open_constr list -> hint_db list -> Proof_type.tactic
 
 val autounfold : hint_db_name list -> Locus.clause -> unit Proofview.tactic
 val autounfold_tac : hint_db_name list option -> Locus.clause -> unit Proofview.tactic
diff --git a/tactics/elim.mli b/tactics/elim.mli
index 05e5c7df2..29c441463 100644
--- a/tactics/elim.mli
+++ b/tactics/elim.mli
@@ -10,11 +10,12 @@ open Names
 open Term
 open Tacticals
 open Misctypes
+open Tactypes
 
 (** Eliminations tactics. *)
 
 val introCaseAssumsThen : evars_flag ->
-  (Tacexpr.intro_patterns -> branch_assumptions -> unit Proofview.tactic) ->
+  (intro_patterns -> branch_assumptions -> unit Proofview.tactic) ->
     branch_args -> unit Proofview.tactic
 
 val h_decompose       : inductive list -> constr -> unit Proofview.tactic
diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml
index b1d3290aa..1a67bedc2 100644
--- a/tactics/eqdecide.ml
+++ b/tactics/eqdecide.ml
@@ -22,6 +22,7 @@ open Tacticals.New
 open Auto
 open Constr_matching
 open Misctypes
+open Tactypes
 open Hipattern
 open Pretyping
 open Tacmach.New
@@ -73,7 +74,7 @@ let mkBranches c1 c2 =
 
 let discrHyp id =
   let c = { delayed = fun env sigma -> Sigma.here (Term.mkVar id, NoBindings) sigma } in
-  let tac c = Equality.discr_tac false (Some (None, Tacexpr.ElimOnConstr c)) in
+  let tac c = Equality.discr_tac false (Some (None, ElimOnConstr c)) in
   Tacticals.New.tclDELAYEDWITHHOLES false c tac
 
 let solveNoteqBranch side =
@@ -121,7 +122,7 @@ let eqCase tac =
 
 let injHyp id =
   let c = { delayed = fun env sigma -> Sigma.here (Term.mkVar id, NoBindings) sigma } in
-  let tac c = Equality.injClause None false (Some (None, Tacexpr.ElimOnConstr c)) in
+  let tac c = Equality.injClause None false (Some (None, ElimOnConstr c)) in
   Tacticals.New.tclDELAYEDWITHHOLES false c tac
 
 let diseqCase hyps eqonleft =
diff --git a/tactics/equality.ml b/tactics/equality.ml
index d4b372837..b525b3ab5 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -26,7 +26,6 @@ open Retyping
 open Tacmach.New
 open Logic
 open Hipattern
-open Tacexpr
 open Tacticals.New
 open Tactics
 open Tacred
diff --git a/tactics/equality.mli b/tactics/equality.mli
index 47cb6b82f..6a4a8126e 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -11,10 +11,10 @@ open Names
 open Term
 open Evd
 open Environ
-open Tacexpr
 open Ind_tables
 open Locus
 open Misctypes
+open Tactypes
 (*i*)
 
 type dep_proof_flag = bool (* true = support rewriting dependent proofs *)
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 4be4d1ed4..ac945de3c 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -20,6 +20,7 @@ open Namegen
 open Libnames
 open Smartlocate
 open Misctypes
+open Tactypes
 open Evd
 open Termops
 open Inductiveops
@@ -40,7 +41,7 @@ module NamedDecl = Context.Named.Declaration
 (* General functions                    *)
 (****************************************)
 
-type debug = Tacexpr.debug = Debug | Info | Off
+type debug = Debug | Info | Off
 
 exception Bound
 
@@ -1231,7 +1232,7 @@ let add_hint_lemmas env sigma eapply lems hint_db =
 let make_local_hint_db env sigma ts eapply lems =
   let map c =
     let sigma = Sigma.Unsafe.of_evar_map sigma in
-    let Sigma (c, sigma, _) = c.Pretyping.delayed env sigma in
+    let Sigma (c, sigma, _) = c.delayed env sigma in
     (Sigma.to_evar_map sigma, c)
   in
   let lems = List.map map lems in
diff --git a/tactics/hints.mli b/tactics/hints.mli
index 83876be84..9a3817203 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -15,6 +15,7 @@ open Globnames
 open Decl_kinds
 open Evd
 open Misctypes
+open Tactypes
 open Clenv
 open Pattern
 open Vernacexpr
@@ -25,7 +26,7 @@ exception Bound
 
 val decompose_app_bound : constr -> global_reference * constr array
 
-type debug = Tacexpr.debug = Debug | Info | Off
+type debug = Debug | Info | Off
 
 (** Pre-created hint databases *)
 
@@ -215,7 +216,7 @@ val repr_hint : hint -> (raw_hint * clausenv) hint_ast
    Useful to take the current goal hypotheses as hints;
    Boolean tells if lemmas with evars are allowed *)
 
-val make_local_hint_db : env -> evar_map -> ?ts:transparent_state -> bool -> Pretyping.delayed_open_constr list -> hint_db
+val make_local_hint_db : env -> evar_map -> ?ts:transparent_state -> bool -> delayed_open_constr list -> hint_db
 
 val make_db_list : hint_db_name list -> hint_db list
 
diff --git a/tactics/inv.ml b/tactics/inv.ml
index c7567dee0..e7d8249e4 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -25,7 +25,6 @@ open Tactics
 open Elim
 open Equality
 open Misctypes
-open Tacexpr
 open Sigma.Notations
 open Proofview.Notations
 
diff --git a/tactics/inv.mli b/tactics/inv.mli
index af1cb996a..df629e7c9 100644
--- a/tactics/inv.mli
+++ b/tactics/inv.mli
@@ -9,7 +9,7 @@
 open Names
 open Term
 open Misctypes
-open Tacexpr
+open Tactypes
 
 type inversion_status = Dep of constr option | NoDep
 
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 2a024aa56..f739488aa 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -15,6 +15,7 @@ open Termops
 open Declarations
 open Tacmach
 open Clenv
+open Tactypes
 open Sigma.Notations
 
 module NamedDecl = Context.Named.Declaration
@@ -152,7 +153,7 @@ type branch_args = {
   nassums    : int;         (* number of assumptions/letin to be introduced *)
   branchsign : bool list;   (* the signature of the branch.
                                true=assumption, false=let-in *)
-  branchnames : Tacexpr.intro_patterns}
+  branchnames : intro_patterns}
 
 type branch_assumptions = {
   ba        : branch_args;       (* the branch args *)
@@ -533,7 +534,7 @@ module New = struct
     Proofview.Goal.nf_enter { enter = begin fun gl ->
       let env = Proofview.Goal.env gl in
       let sigma = Proofview.Goal.sigma gl in
-      let Sigma (x, sigma, _) = x.Pretyping.delayed env sigma in
+      let Sigma (x, sigma, _) = x.delayed env sigma in
       tclWITHHOLES check (tac x) (Sigma.to_evar_map sigma)
     end }
 
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index cfdc2cffd..18cf03c51 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -11,9 +11,9 @@ open Names
 open Term
 open Tacmach
 open Proof_type
-open Tacexpr
 open Locus
 open Misctypes
+open Tactypes
 
 (** Tacticals i.e. functions from tactics to tactics. *)
 
@@ -221,7 +221,7 @@ module New : sig
   val tclCOMPLETE : 'a tactic -> 'a tactic
   val tclSOLVE : unit tactic list -> unit tactic
   val tclPROGRESS : unit tactic -> unit tactic
-  val tclSELECT : goal_selector -> 'a tactic -> 'a tactic
+  val tclSELECT : Vernacexpr.goal_selector -> 'a tactic -> 'a tactic
   val tclWITHHOLES : bool -> 'a tactic -> Evd.evar_map -> 'a tactic
   val tclDELAYEDWITHHOLES : bool -> 'a delayed_open -> ('a -> unit tactic) -> unit tactic
 
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index cae45f607..9d0e9f084 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -32,7 +32,6 @@ open Refiner
 open Tacticals
 open Hipattern
 open Coqlib
-open Tacexpr
 open Decl_kinds
 open Evarutil
 open Indrec
@@ -41,6 +40,7 @@ open Unification
 open Locus
 open Locusops
 open Misctypes
+open Tactypes
 open Proofview.Notations
 open Sigma.Notations
 open Context.Named.Declaration
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index fb033363e..7acfb6286 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -15,10 +15,10 @@ open Evd
 open Clenv
 open Redexpr
 open Globnames
-open Tacexpr
 open Pattern
 open Unification
 open Misctypes
+open Tactypes
 open Locus
 
 (** Main tactics defined in ML. This file is huge and should probably be split