Untangling Tacexpr from lower strata.

15 files changed, 37 insertions, 31 deletions

diff --git a/tactics/auto.mli b/tactics/auto.mli
index f68190498f..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
 
@@ -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 5ed8e439e7..bac4d27c36 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 5007178174..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 : 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 05e5c7df29..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 : 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 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 4be4d1ed4b..ac945de3c9 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 83876be848..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,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 c7567dee03..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
 
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/tacticals.ml b/tactics/tacticals.ml
index 2a024aa562..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 *)
@@ -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 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 cae45f6070..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
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