Make the Coq codebase independent from Ltac-related code.

We untangle many dependencies on Ltac datastructures and modules from the
lower strata, resulting in a self-contained ltac/ folder. While not a plugin
yet, the change is now very easy to perform. The main API changes have been
documented in the dev/doc/changes file.

The patches are quite rough, and it may be the case that some parts of the
code can migrate back from ltac/ to a core folder. This should be decided on
a case-by-case basis, according to a more long-term consideration of what is
exactly Ltac-dependent and whatnot.

21 files changed, 67 insertions, 490 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 962af4b5c5..b85328402d 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -20,7 +20,6 @@ open Genredexpr
 open Tactics
 open Tacticals
 open Clenv
-open Tacexpr
 open Locus
 open Proofview.Notations
 open Hints
diff --git a/tactics/auto.mli b/tactics/auto.mli
index 1608a0ea63..1689bd73c7 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
 
@@ -39,45 +40,45 @@ val conclPattern : constr -> constr_pattern option -> Genarg.glob_generic_argume
 (** The use of the "core" database can be de-activated by passing
     "nocore" amongst the databases. *)
 
-val auto : ?debug:Tacexpr.debug ->
-  int -> Tacexpr.delayed_open_constr list -> hint_db_name list -> unit Proofview.tactic
+val auto : ?debug:debug ->
+  int -> delayed_open_constr list -> hint_db_name list -> unit Proofview.tactic
 
 (** Auto with more delta. *)
 
-val new_auto : ?debug:Tacexpr.debug ->
-  int -> Tacexpr.delayed_open_constr list -> hint_db_name list -> unit Proofview.tactic
+val new_auto : ?debug:debug ->
+  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:Tacexpr.debug ->
-  int -> Tacexpr.delayed_open_constr list -> unit Proofview.tactic
+val full_auto : ?debug:debug ->
+  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:Tacexpr.debug ->
-  int -> Tacexpr.delayed_open_constr list -> unit Proofview.tactic
+val new_full_auto : ?debug:debug ->
+  int -> delayed_open_constr list -> unit Proofview.tactic
 
 (** auto with default search depth and with all hint databases
    except the "v62" compatibility database *)
 val default_full_auto : unit Proofview.tactic
 
 (** The generic form of auto (second arg [None] means all bases) *)
-val gen_auto : ?debug:Tacexpr.debug ->
-  int option -> Tacexpr.delayed_open_constr list -> hint_db_name list option -> unit Proofview.tactic
+val gen_auto : ?debug:debug ->
+  int option -> delayed_open_constr list -> hint_db_name list option -> unit Proofview.tactic
 
 (** The hidden version of auto *)
-val h_auto   : ?debug:Tacexpr.debug ->
-  int option -> Tacexpr.delayed_open_constr list -> hint_db_name list option -> unit Proofview.tactic
+val h_auto   : ?debug:debug ->
+  int option -> delayed_open_constr list -> hint_db_name list option -> unit Proofview.tactic
 
 (** Trivial *)
 
-val trivial : ?debug:Tacexpr.debug ->
-  Tacexpr.delayed_open_constr list -> hint_db_name list -> unit Proofview.tactic
-val gen_trivial : ?debug:Tacexpr.debug ->
-  Tacexpr.delayed_open_constr list -> hint_db_name list option -> unit Proofview.tactic
-val full_trivial : ?debug:Tacexpr.debug ->
-  Tacexpr.delayed_open_constr list -> unit Proofview.tactic
-val h_trivial : ?debug:Tacexpr.debug ->
-  Tacexpr.delayed_open_constr list -> hint_db_name list option -> unit Proofview.tactic
+val trivial : ?debug:debug ->
+  delayed_open_constr list -> hint_db_name list -> unit Proofview.tactic
+val gen_trivial : ?debug:debug ->
+  delayed_open_constr list -> hint_db_name list option -> unit Proofview.tactic
+val full_trivial : ?debug:debug ->
+  delayed_open_constr list -> unit Proofview.tactic
+val h_trivial : ?debug:debug ->
+  delayed_open_constr list -> hint_db_name list option -> unit Proofview.tactic
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index 7628b7885f..dae1cc9f1b 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -83,7 +83,7 @@ let print_rewrite_hintdb bas =
 	     str (if h.rew_l2r then "rewrite -> " else "rewrite <- ") ++
 	       Printer.pr_lconstr h.rew_lemma ++ str " of type " ++ Printer.pr_lconstr h.rew_type ++
 	       Option.cata (fun tac -> str " then use tactic " ++
-	       Pptactic.pr_glb_generic (Global.env()) tac) (mt ()) h.rew_tac)
+	       Pputils.pr_glb_generic (Global.env()) tac) (mt ()) h.rew_tac)
 	   (find_rewrites bas))
 
 type raw_rew_rule = Loc.t * constr Univ.in_universe_context_set * bool * Genarg.raw_generic_argument option
diff --git a/tactics/autorewrite.mli b/tactics/autorewrite.mli
index 0706571795..49e8588da3 100644
--- a/tactics/autorewrite.mli
+++ b/tactics/autorewrite.mli
@@ -9,7 +9,6 @@
 (** This files implements the autorewrite tactic. *)
 
 open Term
-open Tacexpr
 open Equality
 
 (** Rewriting rules before tactic interpretation *)
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index ba21950707..bac4d27c36 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -20,7 +20,7 @@ open Tactics
 open Clenv
 open Auto
 open Genredexpr
-open Tacexpr
+open Tactypes
 open Locus
 open Locusops
 open Hints
@@ -203,7 +203,7 @@ type search_state = {
   dblist : hint_db list;
   localdb :  hint_db list;
   prev : prev_search_state;
-  local_lemmas : Tacexpr.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 8812093d5f..1f69e4ab3c 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 : Tacexpr.delayed_open_constr list -> int -> unit Proofview.tactic
+val prolog_tac : delayed_open_constr list -> int -> unit Proofview.tactic
 
-val gen_eauto : ?debug:Tacexpr.debug -> bool * int -> Tacexpr.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:Tacexpr.debug ->
+  ?debug:debug ->
   bool * int ->
-  Tacexpr.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 ae9cf85f3c..29c4414636 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 : Tacexpr.evars_flag ->
-  (Tacexpr.intro_patterns -> branch_assumptions -> unit Proofview.tactic) ->
+val introCaseAssumsThen : evars_flag ->
+  (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 b1d3290aac..1a67bedc28 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 d4b372837d..b525b3ab56 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 47cb6b82fd..6a4a8126e1 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 4b43a9e696..ac945de3c9 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -20,11 +20,11 @@ open Namegen
 open Libnames
 open Smartlocate
 open Misctypes
+open Tactypes
 open Evd
 open Termops
 open Inductiveops
 open Typing
-open Tacexpr
 open Decl_kinds
 open Pattern
 open Patternops
@@ -41,6 +41,8 @@ module NamedDecl = Context.Named.Declaration
 (* General functions                    *)
 (****************************************)
 
+type debug = Debug | Info | Off
+
 exception Bound
 
 let head_constr_bound t =
@@ -803,7 +805,6 @@ let make_unfold eref =
      code = with_uid (Unfold_nth eref) })
 
 let make_extern pri pat tacast =
-  let tacast = Genarg.in_gen (Genarg.glbwit Constrarg.wit_ltac) tacast in
   let hdconstr = Option.map try_head_pattern pat in
   (hdconstr,
    { pri = pri;
@@ -1081,8 +1082,6 @@ let add_trivials env sigma l local dbnames =
       Lib.add_anonymous_leaf (inAutoHint hint))
     dbnames
 
-let (forward_intern_tac, extern_intern_tac) = Hook.make ()
-
 type hnf = bool
 
 type hints_entry =
@@ -1093,7 +1092,7 @@ type hints_entry =
   | HintsTransparencyEntry of evaluable_global_reference list * bool
   | HintsModeEntry of global_reference * hint_mode list
   | HintsExternEntry of
-      int * (patvar list * constr_pattern) option * glob_tactic_expr
+      int * (patvar list * constr_pattern) option * Genarg.glob_generic_argument
 
 let default_prepare_hint_ident = Id.of_string "H"
 
@@ -1183,7 +1182,9 @@ let interp_hints poly =
   | HintsExtern (pri, patcom, tacexp) ->
       let pat =	Option.map fp patcom in
       let l = match pat with None -> [] | Some (l, _) -> l in
-      let tacexp = Hook.get forward_intern_tac l tacexp in
+      let ltacvars = List.fold_left (fun accu x -> Id.Set.add x accu) Id.Set.empty l in
+      let env = Genintern.({ genv = env; ltacvars }) in
+      let _, tacexp = Genintern.generic_intern env tacexp in
       HintsExternEntry (pri, pat, tacexp)
 
 let add_hints local dbnames0 h =
@@ -1276,7 +1277,7 @@ let pr_hint h = match h.obj with
           env
         with e when CErrors.noncritical e -> Global.env ()
       in
-      (str "(*external*) " ++ Pptactic.pr_glb_generic env tac)
+      (str "(*external*) " ++ Pputils.pr_glb_generic env tac)
 
 let pr_id_hint (id, v) =
   (pr_hint v.code ++ str"(level " ++ int v.pri ++ str", id " ++ int id ++ str ")" ++ spc ())
diff --git a/tactics/hints.mli b/tactics/hints.mli
index 6f5ee8ba5e..9a38172035 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,6 +26,8 @@ exception Bound
 
 val decompose_app_bound : constr -> global_reference * constr array
 
+type debug = Debug | Info | Off
+
 (** Pre-created hint databases *)
 
 type 'a hint_ast =
@@ -132,7 +135,7 @@ type hints_entry =
   | HintsTransparencyEntry of evaluable_global_reference list * bool
   | HintsModeEntry of global_reference * hint_mode list
   | HintsExternEntry of
-      int * (patvar list * constr_pattern) option * Tacexpr.glob_tactic_expr
+      int * (patvar list * constr_pattern) option * Genarg.glob_generic_argument
 
 val searchtable_map : hint_db_name -> hint_db
 
@@ -199,7 +202,7 @@ val make_resolve_hyp :
 (** [make_extern pri pattern tactic_expr] *)
 
 val make_extern :
-  int -> constr_pattern option -> Tacexpr.glob_tactic_expr
+  int -> constr_pattern option -> Genarg.glob_generic_argument
       -> hint_entry
 
 val run_hint : hint ->
@@ -209,14 +212,11 @@ val run_hint : hint ->
     written code. *)
 val repr_hint : hint -> (raw_hint * clausenv) hint_ast
 
-val extern_intern_tac :
-  (patvar list -> Tacexpr.raw_tactic_expr -> Tacexpr.glob_tactic_expr) Hook.t
-
 (** Create a Hint database from the pairs (name, constr).
    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 -> Tacexpr.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 291bc09650..e7d8249e43 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
 
@@ -497,8 +496,6 @@ let inversion inv_kind status names id =
 let inv_gen thin status names =
   try_intros_until (inversion thin status names)
 
-open Tacexpr
-
 let inv k = inv_gen k NoDep
 
 let inv_tac id       = inv FullInversion None (NamedHyp id)
diff --git a/tactics/inv.mli b/tactics/inv.mli
index af1cb996a5..df629e7c9f 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/tactic_matching.ml b/tactics/tactic_matching.ml
deleted file mode 100644
index ef45ee47e1..0000000000
--- a/tactics/tactic_matching.ml
+++ /dev/null
@@ -1,377 +0,0 @@
-(************************************************************************)
-(*  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        *)
-(************************************************************************)
-
-(** This file extends Matching with the main logic for Ltac's
-    (lazy)match and (lazy)match goal. *)
-
-open Names
-open Tacexpr
-open Context.Named.Declaration
-
-module NamedDecl = Context.Named.Declaration
-
-(** [t] is the type of matching successes. It ultimately contains a
-    {!Tacexpr.glob_tactic_expr} representing the left-hand side of the
-    corresponding matching rule, a matching substitution to be
-    applied, a context substitution mapping identifier to context like
-    those of {!Matching.matching_result}), and a {!Term.constr}
-    substitution mapping corresponding to matched hypotheses. *)
-type 'a t = {
-  subst : Constr_matching.bound_ident_map * Pattern.extended_patvar_map ;
-  context : Term.constr Id.Map.t;
-  terms : Term.constr Id.Map.t;
-  lhs : 'a;
-}
-
-
-
-(** {6 Utilities} *)
-
-
-(** Some of the functions of {!Matching} return the substitution with a
-    [patvar_map] instead of an [extended_patvar_map]. [adjust] coerces
-    substitution of the former type to the latter. *)
-let adjust : Constr_matching.bound_ident_map * Pattern.patvar_map ->
-             Constr_matching.bound_ident_map * Pattern.extended_patvar_map =
-  fun (l, lc) -> (l, Id.Map.map (fun c -> [], c) lc)
-
-
-(** Adds a binding to a {!Id.Map.t} if the identifier is [Some id] *)
-let id_map_try_add id x m =
-  match id with
-  | Some id -> Id.Map.add id x m
-  | None -> m
-
-(** Adds a binding to a {!Id.Map.t} if the name is [Name id] *)
-let id_map_try_add_name id x m =
-  match id with
-  | Name id -> Id.Map.add id x m
-  | Anonymous -> m
-
-(** Takes the union of two {!Id.Map.t}. If there is conflict,
-    the binding of the right-hand argument shadows that of the left-hand
-    argument. *)
-let id_map_right_biased_union m1 m2 =
-  if Id.Map.is_empty m1 then m2 (** Don't reconstruct the whole map *)
-  else Id.Map.fold Id.Map.add m2 m1
-
-(** Tests whether the substitution [s] is empty. *)
-let is_empty_subst (ln,lm) =
-  Id.Map.(is_empty ln && is_empty lm)
-
-(** {6 Non-linear patterns} *)
-
-
-(** The patterns of Ltac are not necessarily linear. Non-linear
-    pattern are partially handled by the {!Matching} module, however
-    goal patterns are not primitive to {!Matching}, hence we must deal
-    with non-linearity between hypotheses and conclusion. Subterms are
-    considered equal up to the equality implemented in
-    [equal_instances]. *)
-(* spiwack: it doesn't seem to be quite the same rule for non-linear
-   term patterns and non-linearity between hypotheses and/or
-   conclusion. Indeed, in [Matching], matching is made modulo
-   syntactic equality, and here we merge modulo conversion. It may be
-   a good idea to have an entry point of [Matching] with a partial
-   substitution as argument instead of merging substitution here. That
-   would ensure consistency. *)
-let equal_instances env sigma (ctx',c') (ctx,c) =
-  (* How to compare instances? Do we want the terms to be convertible?
-     unifiable? Do we want the universe levels to be relevant? 
-     (historically, conv_x is used) *)
-  CList.equal Id.equal ctx ctx' && Reductionops.is_conv env sigma c' c
-
-
-(** Merges two substitutions. Raises [Not_coherent_metas] when
-    encountering two instances of the same metavariable which are not
-    equal according to {!equal_instances}. *)
-exception Not_coherent_metas
-let verify_metas_coherence env sigma (ln1,lcm) (ln,lm) =
-  let merge id oc1 oc2 = match oc1, oc2 with
-    | None, None -> None
-    | None, Some c | Some c, None -> Some c
-    | Some c1, Some c2 ->
-        if equal_instances env sigma c1 c2 then Some c1
-        else raise Not_coherent_metas
-  in
-  let (+++) lfun1 lfun2 = Id.Map.fold Id.Map.add lfun1 lfun2 in
-  (** ppedrot: Is that even correct? *)
-  let merged = ln +++ ln1 in
-  (merged, Id.Map.merge merge lcm lm)
-
-let matching_error =
-  CErrors.UserError (Some "tactic matching" , Pp.str "No matching clauses for match.")
-
-let imatching_error = (matching_error, Exninfo.null)
-
-(** A functor is introduced to share the environment and the
-    evar_map. They do not change and it would be a pity to introduce
-    closures everywhere just for the occasional calls to
-    {!equal_instances}. *)
-module type StaticEnvironment = sig
-  val env : Environ.env
-  val sigma : Evd.evar_map
-end
-module PatternMatching (E:StaticEnvironment) = struct
-
-
-  (** {6 The pattern-matching monad } *)
-
-
-  (** To focus on the algorithmic portion of pattern-matching, the
-      bookkeeping is relegated to a monad: the composition of the
-      bactracking monad of {!IStream.t} with a "writer" effect. *)
-  (* spiwack: as we don't benefit from the various stream optimisations
-     of Haskell, it may be costly to give the monad in direct style such as
-     here. We may want to use some continuation passing style. *)
-  type 'a tac = 'a Proofview.tactic
-  type 'a m = { stream : 'r. ('a -> unit t -> 'r tac) -> unit t -> 'r tac }
-
-  (** The empty substitution. *)
-  let empty_subst = Id.Map.empty , Id.Map.empty
-
-  (** Composes two substitutions using {!verify_metas_coherence}. It
-      must be a monoid with neutral element {!empty_subst}. Raises
-      [Not_coherent_metas] when composition cannot be achieved. *)
-  let subst_prod s1 s2 =
-    if is_empty_subst s1 then s2
-    else if is_empty_subst s2 then s1
-    else verify_metas_coherence E.env E.sigma s1 s2
-
-  (** The empty context substitution. *)
-  let empty_context_subst = Id.Map.empty
-
-  (** Compose two context substitutions, in case of conflict the
-      right hand substitution shadows the left hand one. *)
-  let context_subst_prod = id_map_right_biased_union
-
-  (** The empty term substitution. *)
-  let empty_term_subst = Id.Map.empty
-
-  (** Compose two terms substitutions, in case of conflict the
-      right hand substitution shadows the left hand one. *)
-  let term_subst_prod = id_map_right_biased_union
-
-  (** Merge two writers (and ignore the first value component). *)
-  let merge m1 m2 =
-    try Some {
-      subst = subst_prod m1.subst m2.subst;
-      context = context_subst_prod m1.context m2.context;
-      terms = term_subst_prod m1.terms m2.terms;
-      lhs = m2.lhs;
-    }
-    with Not_coherent_metas -> None
-
-  (** Monadic [return]: returns a single success with empty substitutions. *)
-  let return (type a) (lhs:a) : a m =
-    { stream = fun k ctx -> k lhs ctx }
-
-  (** Monadic bind: each success of [x] is replaced by the successes
-      of [f x]. The substitutions of [x] and [f x] are composed,
-      dropping the apparent successes when the substitutions are not
-      coherent. *)
-  let (>>=) (type a) (type b) (m:a m) (f:a -> b m) : b m =
-    { stream = fun k ctx -> m.stream (fun x ctx -> (f x).stream k ctx) ctx }
-
-  (** A variant of [(>>=)] when the first argument returns [unit]. *)
-  let (<*>) (type a) (m:unit m) (y:a m) : a m =
-    { stream = fun k ctx -> m.stream (fun () ctx -> y.stream k ctx) ctx }
-
-  (** Failure of the pattern-matching monad: no success. *)
-  let fail (type a) : a m = { stream = fun _ _ -> Proofview.tclZERO matching_error }
-
-  let run (m : 'a m) =
-    let ctx = {
-      subst = empty_subst ;
-      context = empty_context_subst ;
-      terms = empty_term_subst ;
-      lhs = ();
-    } in
-    let eval lhs ctx = Proofview.tclUNIT { ctx with lhs } in
-    m.stream eval ctx
-
-  (** Chooses in a list, in the same order as the list *)
-  let rec pick (l:'a list) (e, info) : 'a m = match l with
-  | [] -> { stream = fun _ _ -> Proofview.tclZERO ~info e }
-  | x :: l ->
-    { stream = fun k ctx -> Proofview.tclOR (k x ctx) (fun e -> (pick l e).stream k ctx) }
-
-  let pick l = pick l imatching_error
-
-  (** Declares a subsitution, a context substitution and a term substitution. *)
-  let put subst context terms : unit m =
-    let s = { subst ; context ; terms ; lhs = () } in
-    { stream = fun k ctx -> match merge s ctx with None -> Proofview.tclZERO matching_error | Some s -> k () s }
-
-  (** Declares a substitution. *)
-  let put_subst subst : unit m = put subst empty_context_subst empty_term_subst
-
-  (** Declares a term substitution. *)
-  let put_terms terms : unit m = put empty_subst empty_context_subst terms
-
-
-
-  (** {6 Pattern-matching} *)
-
-
-  (** [wildcard_match_term lhs] matches a term against a wildcard
-      pattern ([_ => lhs]). It has a single success with an empty
-      substitution. *)
-  let wildcard_match_term = return
-
-  (** [pattern_match_term refresh pat term lhs] returns the possible
-      matchings of [term] with the pattern [pat => lhs]. If refresh is
-      true, refreshes the universes of [term]. *)
-  let pattern_match_term refresh pat term lhs = 
-(*     let term = if refresh then Termops.refresh_universes_strict term else term in *)
-    match pat with
-    | Term p ->
-        begin 
-          try
-            put_subst (Constr_matching.extended_matches E.env E.sigma p term) <*>
-            return lhs
-          with Constr_matching.PatternMatchingFailure -> fail
-        end
-    | Subterm (with_app_context,id_ctxt,p) ->
-
-      let rec map s (e, info) =
-        { stream = fun k ctx -> match IStream.peek s with
-          | IStream.Nil -> Proofview.tclZERO ~info e
-          | IStream.Cons ({ Constr_matching.m_sub ; m_ctx }, s) ->
-            let subst = adjust m_sub in
-            let context = id_map_try_add id_ctxt m_ctx Id.Map.empty in
-            let terms = empty_term_subst in
-            let nctx = { subst ; context ; terms ; lhs = () } in
-            match merge ctx nctx with
-            | None -> (map s (e, info)).stream k ctx
-            | Some nctx -> Proofview.tclOR (k lhs nctx) (fun e -> (map s e).stream k ctx)
-        }
-      in
-      map (Constr_matching.match_subterm_gen E.env E.sigma with_app_context p term) imatching_error
-
-
-  (** [rule_match_term term rule] matches the term [term] with the
-      matching rule [rule]. *)
-  let rule_match_term term = function
-    | All lhs -> wildcard_match_term lhs
-    | Pat ([],pat,lhs) -> pattern_match_term false pat term lhs
-    | Pat _ ->
-        (** Rules with hypotheses, only work in match goal. *)
-        fail
-
-  (** [match_term term rules] matches the term [term] with the set of
-      matching rules [rules].*)
-  let rec match_term (e, info) term rules = match rules with
-  | [] -> { stream = fun _ _ -> Proofview.tclZERO ~info e }
-  | r :: rules ->
-    { stream = fun k ctx ->
-      let head = rule_match_term term r in
-      let tail e = match_term e term rules in
-      Proofview.tclOR (head.stream k ctx) (fun e -> (tail e).stream k ctx)
-    }
-
-
-  (** [hyp_match_type hypname pat hyps] matches a single
-      hypothesis pattern [hypname:pat] against the hypotheses in
-      [hyps]. Tries the hypotheses in order. For each success returns
-      the name of the matched hypothesis. *)
-  let hyp_match_type hypname pat hyps =
-    pick hyps >>= fun decl ->
-    let id = NamedDecl.get_id decl in
-    let refresh = is_local_def decl in
-    pattern_match_term refresh pat (NamedDecl.get_type decl) () <*>
-    put_terms (id_map_try_add_name hypname (Term.mkVar id) empty_term_subst) <*>
-    return id
-
-  (** [hyp_match_type hypname bodypat typepat hyps] matches a single
-      hypothesis pattern [hypname := bodypat : typepat] against the
-      hypotheses in [hyps].Tries the hypotheses in order. For each
-      success returns the name of the matched hypothesis. *)
-  let hyp_match_body_and_type hypname bodypat typepat hyps =
-    pick hyps >>= function
-      | LocalDef (id,body,hyp) ->
-          pattern_match_term false bodypat body () <*>
-          pattern_match_term true typepat hyp () <*>
-          put_terms (id_map_try_add_name hypname (Term.mkVar id) empty_term_subst) <*>
-          return id
-      | LocalAssum (id,hyp) -> fail
-
-  (** [hyp_match pat hyps] dispatches to
-      {!hyp_match_type} or {!hyp_match_body_and_type} depending on whether
-      [pat] is [Hyp _] or [Def _]. *)
-  let hyp_match pat hyps =
-    match pat with
-    | Hyp ((_,hypname),typepat) ->
-        hyp_match_type hypname typepat hyps
-    | Def ((_,hypname),bodypat,typepat) ->
-        hyp_match_body_and_type hypname bodypat typepat hyps
-
-  (** [hyp_pattern_list_match pats hyps lhs], matches the list of
-      patterns [pats] against the hypotheses in [hyps], and eventually
-      returns [lhs]. *)
-  let rec hyp_pattern_list_match pats hyps lhs =
-    match pats with
-    | pat::pats ->
-        hyp_match pat hyps >>= fun matched_hyp ->
-        (* spiwack: alternatively it is possible to return the list
-           with the matched hypothesis removed directly in
-           [hyp_match]. *)
-        let select_matched_hyp decl = Id.equal (NamedDecl.get_id decl) matched_hyp in
-        let hyps = CList.remove_first select_matched_hyp hyps in
-        hyp_pattern_list_match pats hyps lhs
-    | [] -> return lhs
-
-  (** [rule_match_goal hyps concl rule] matches the rule [rule]
-      against the goal [hyps|-concl]. *)
-  let rule_match_goal hyps concl = function
-    | All lhs -> wildcard_match_term lhs
-    | Pat (hyppats,conclpat,lhs) ->
-        (* the rules are applied from the topmost one (in the concrete
-           syntax) to the bottommost. *)
-        let hyppats = List.rev hyppats in
-        pattern_match_term false conclpat concl () <*>
-        hyp_pattern_list_match hyppats hyps lhs
-
-  (** [match_goal hyps concl rules] matches the goal [hyps|-concl]
-      with the set of matching rules [rules]. *)
-  let rec match_goal (e, info) hyps concl rules = match rules with
-  | [] -> { stream = fun _ _ -> Proofview.tclZERO ~info e }
-  | r :: rules ->
-    { stream = fun k ctx ->
-      let head = rule_match_goal hyps concl r in
-      let tail e = match_goal e hyps concl rules in
-      Proofview.tclOR (head.stream k ctx) (fun e -> (tail e).stream k ctx)
-    }
-
-end
-
-(** [match_term env sigma term rules] matches the term [term] with the
-    set of matching rules [rules]. The environment [env] and the
-    evar_map [sigma] are not currently used, but avoid code
-    duplication. *)
-let match_term env sigma term rules =
-  let module E = struct
-    let env = env
-    let sigma = sigma
-  end in
-  let module M = PatternMatching(E) in
-  M.run (M.match_term imatching_error term rules)
-
-
-(** [match_goal env sigma hyps concl rules] matches the goal
-    [hyps|-concl] with the set of matching rules [rules]. The
-    environment [env] and the evar_map [sigma] are used to check
-    convertibility for pattern variables shared between hypothesis
-    patterns or the conclusion pattern. *)
-let match_goal env sigma hyps concl rules =
-  let module E = struct
-    let env = env
-    let sigma = sigma
-  end in
-  let module M = PatternMatching(E) in
-  M.run (M.match_goal imatching_error hyps concl rules)
diff --git a/tactics/tactic_matching.mli b/tactics/tactic_matching.mli
deleted file mode 100644
index 090207bcc3..0000000000
--- a/tactics/tactic_matching.mli
+++ /dev/null
@@ -1,49 +0,0 @@
- (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(** This file extends Matching with the main logic for Ltac's
-    (lazy)match and (lazy)match goal. *)
-
-
-(** [t] is the type of matching successes. It ultimately contains a
-    {!Tacexpr.glob_tactic_expr} representing the left-hand side of the
-    corresponding matching rule, a matching substitution to be
-    applied, a context substitution mapping identifier to context like
-    those of {!Matching.matching_result}), and a {!Term.constr}
-    substitution mapping corresponding to matched hypotheses. *)
-type 'a t = {
-  subst : Constr_matching.bound_ident_map * Pattern.extended_patvar_map ;
-  context : Term.constr Names.Id.Map.t;
-  terms : Term.constr Names.Id.Map.t;
-  lhs : 'a;
-}
-
-
-(** [match_term env sigma term rules] matches the term [term] with the
-    set of matching rules [rules]. The environment [env] and the
-    evar_map [sigma] are not currently used, but avoid code
-    duplication. *)
-val match_term :
-  Environ.env ->
-  Evd.evar_map ->
-  Term.constr ->
-  (Tacexpr.binding_bound_vars * Pattern.constr_pattern, Tacexpr.glob_tactic_expr) Tacexpr.match_rule list ->
-  Tacexpr.glob_tactic_expr t Proofview.tactic
-
-(** [match_goal env sigma hyps concl rules] matches the goal
-    [hyps|-concl] with the set of matching rules [rules]. The
-    environment [env] and the evar_map [sigma] are used to check
-    convertibility for pattern variables shared between hypothesis
-    patterns or the conclusion pattern. *)
-val match_goal:
-  Environ.env ->
-  Evd.evar_map ->
-  Context.Named.t ->
-  Term.constr ->
-  (Tacexpr.binding_bound_vars * Pattern.constr_pattern, Tacexpr.glob_tactic_expr) Tacexpr.match_rule list ->
-  Tacexpr.glob_tactic_expr t Proofview.tactic
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 203d975428..f739488aab 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 *)
@@ -479,10 +480,10 @@ module New = struct
 
   (* Select a subset of the goals *)
   let tclSELECT = function
-    | Tacexpr.SelectNth i -> Proofview.tclFOCUS i i
-    | Tacexpr.SelectList l -> Proofview.tclFOCUSLIST l
-    | Tacexpr.SelectId id -> Proofview.tclFOCUSID id
-    | Tacexpr.SelectAll -> fun tac -> tac
+    | Vernacexpr.SelectNth i -> Proofview.tclFOCUS i i
+    | Vernacexpr.SelectList l -> Proofview.tclFOCUSLIST l
+    | Vernacexpr.SelectId id -> Proofview.tclFOCUSID id
+    | Vernacexpr.SelectAll -> fun tac -> tac
 
   (* Check that holes in arguments have been resolved *)
 
@@ -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.Tacexpr.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 cfdc2cffd4..18cf03c51d 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 85b6e8de9e..9d0e9f0842 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
@@ -871,7 +871,11 @@ let reduction_clause redexp cl =
 	(None, bind_red_expr_occurrences occs nbcl redexp)) cl
 
 let reduce redexp cl =
-  let trace () = Pp.(hov 2 (Pptactic.pr_atomic_tactic (Global.env()) (TacReduce (redexp,cl)))) in
+  let trace () =
+    let open Printer in
+    let pr = (pr_constr, pr_lconstr, pr_evaluable_reference, pr_constr_pattern) in
+    Pp.(hov 2 (Pputils.pr_red_expr pr str redexp))
+  in
   Proofview.Trace.name_tactic trace begin
   Proofview.Goal.enter { enter = begin fun gl ->
   let cl' = concrete_clause_of (fun () -> Tacmach.New.pf_ids_of_hyps gl) cl in
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index fb033363e8..7acfb62864 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
diff --git a/tactics/tactics.mllib b/tactics/tactics.mllib
index 093302608e..f54ad86a3f 100644
--- a/tactics/tactics.mllib
+++ b/tactics/tactics.mllib
@@ -16,7 +16,6 @@ Hints
 Auto
 Eauto
 Class_tactics
-Tactic_matching
 Term_dnet
 Eqdecide
 Autorewrite