Unplugging Tacexpr in several interface files.

22 files changed, 60 insertions, 51 deletions

diff --git a/intf/misctypes.mli b/intf/misctypes.mli
index 1452bbc34..c6c4b01e4 100644
--- a/intf/misctypes.mli
+++ b/intf/misctypes.mli
@@ -108,3 +108,12 @@ type 'a or_by_notation =
 (** Kinds of modules *)
 
 type module_kind = Module | ModType | ModAny
+
+(** Various flags *)
+
+type direction_flag = bool (* true = Left-to-right    false = right-to-right *)
+type evars_flag = bool     (* true = pose evars       false = fail on evars *)
+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 *)
diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index 946d124a4..cf33d7973 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -125,7 +125,7 @@ type glob_constr_and_expr = Glob_term.glob_constr * constr_expr option
 type open_constr_expr = unit * constr_expr
 type open_glob_constr = unit * glob_constr_and_expr
 
-type binding_bound_vars = Id.Set.t
+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 =
diff --git a/lib/future.mli b/lib/future.mli
index 114c59176..c780faf32 100644
--- a/lib/future.mli
+++ b/lib/future.mli
@@ -87,7 +87,7 @@ val from_val : ?fix_exn:fix_exn -> 'a -> 'a computation
    the value is not just the 'a but also the global system state *)
 val from_here : ?fix_exn:fix_exn -> 'a -> 'a computation
 
-(* To get the fix_exn of a computation and build a Tacexpr.declaration_hook.
+(* To get the fix_exn of a computation and build a Lemmas.declaration_hook.
  * When a future enters the environment a corresponding hook is run to perform
  * some work.  If this fails, then its failure has to be annotated with the
  * same state id that corresponds to the future computation end.  I.e. Qed
diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml
index 886a98263..5ec44a68d 100644
--- a/pretyping/constr_matching.ml
+++ b/pretyping/constr_matching.ml
@@ -45,6 +45,7 @@ open Context.Rel.Declaration
 
  *)
 
+type binding_bound_vars = Id.Set.t
 type bound_ident_map = Id.t Id.Map.t
 
 exception PatternMatchingFailure
diff --git a/pretyping/constr_matching.mli b/pretyping/constr_matching.mli
index 8d8166f22..ee6c5141b 100644
--- a/pretyping/constr_matching.mli
+++ b/pretyping/constr_matching.mli
@@ -13,6 +13,8 @@ open Term
 open Environ
 open Pattern
 
+type binding_bound_vars = Id.Set.t
+
 (** [PatternMatchingFailure] is the exception raised when pattern
   matching fails *)
 exception PatternMatchingFailure
@@ -41,7 +43,7 @@ val matches_head : env -> Evd.evar_map -> constr_pattern -> constr -> patvar_map
    variables or metavariables have the same name, the metavariable,
    or else the rightmost bound variable, takes precedence *)
 val extended_matches :
-  env -> Evd.evar_map -> Tacexpr.binding_bound_vars * constr_pattern ->
+  env -> Evd.evar_map -> binding_bound_vars * constr_pattern ->
   constr -> bound_ident_map * extended_patvar_map
 
 (** [is_matching pat c] just tells if [c] matches against [pat] *)
@@ -75,7 +77,7 @@ val match_appsubterm : env -> Evd.evar_map -> constr_pattern -> constr -> matchi
 (** [match_subterm_gen] calls either [match_subterm] or [match_appsubterm] *)
 val match_subterm_gen : env -> Evd.evar_map ->
   bool (** true = with app context *) ->
-  Tacexpr.binding_bound_vars * constr_pattern -> constr ->
+  binding_bound_vars * constr_pattern -> constr ->
   matching_result IStream.t
 
 (** [is_matching_appsubterm pat c] tells if a subterm of [c] matches
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 385e100e2..0d9bde2ec 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -61,6 +61,7 @@ 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 824bb11aa..7cb256e4f 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -58,6 +58,8 @@ type inference_flags = {
 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
diff --git a/proofs/clenvtac.mli b/proofs/clenvtac.mli
index aa091aecd..8a096b645 100644
--- a/proofs/clenvtac.mli
+++ b/proofs/clenvtac.mli
@@ -10,8 +10,8 @@
 
 open Term
 open Clenv
-open Tacexpr
 open Unification
+open Misctypes
 
 (** Tactics *)
 val unify : ?flags:unify_flags -> constr -> unit Proofview.tactic
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli
index f7798a0ed..ff60ae5bf 100644
--- a/proofs/proof_type.mli
+++ b/proofs/proof_type.mli
@@ -11,7 +11,6 @@
 open Evd
 open Names
 open Term
-open Tacexpr
 open Glob_term
 open Nametab
 open Misctypes
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 962af4b5c..b85328402 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 1608a0ea6..f68190498 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -39,45 +39,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 -> Pretyping.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 -> Pretyping.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 -> Pretyping.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 -> Pretyping.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 -> Pretyping.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 -> Pretyping.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 ->
+  Pretyping.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
+val full_trivial : ?debug:debug ->
+  Pretyping.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
diff --git a/tactics/autorewrite.mli b/tactics/autorewrite.mli
index 070657179..49e8588da 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 ba2195070..5ed8e439e 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -20,7 +20,6 @@ open Tactics
 open Clenv
 open Auto
 open Genredexpr
-open Tacexpr
 open Locus
 open Locusops
 open Hints
@@ -203,7 +202,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 : Pretyping.delayed_open_constr list;
 }
 
 and prev_search_state = (* for info eauto *)
diff --git a/tactics/eauto.mli b/tactics/eauto.mli
index 8812093d5..500717817 100644
--- a/tactics/eauto.mli
+++ b/tactics/eauto.mli
@@ -16,15 +16,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 : Pretyping.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 -> Pretyping.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
+  Pretyping.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 ae9cf85f3..05e5c7df2 100644
--- a/tactics/elim.mli
+++ b/tactics/elim.mli
@@ -13,7 +13,7 @@ open Misctypes
 
 (** Eliminations tactics. *)
 
-val introCaseAssumsThen : Tacexpr.evars_flag ->
+val introCaseAssumsThen : evars_flag ->
   (Tacexpr.intro_patterns -> branch_assumptions -> unit Proofview.tactic) ->
     branch_args -> unit Proofview.tactic
 
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 4b43a9e69..9ee9e798b 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -24,7 +24,6 @@ open Evd
 open Termops
 open Inductiveops
 open Typing
-open Tacexpr
 open Decl_kinds
 open Pattern
 open Patternops
@@ -41,6 +40,8 @@ module NamedDecl = Context.Named.Declaration
 (* General functions                    *)
 (****************************************)
 
+type debug = Tacexpr.debug = Debug | Info | Off
+
 exception Bound
 
 let head_constr_bound t =
@@ -1093,7 +1094,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 * Tacexpr.glob_tactic_expr
 
 let default_prepare_hint_ident = Id.of_string "H"
 
@@ -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.delayed env sigma in
+    let Sigma (c, sigma, _) = c.Pretyping.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 6d5342e00..e38daca92 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -25,6 +25,8 @@ exception Bound
 
 val decompose_app_bound : constr -> global_reference * constr array
 
+type debug = Tacexpr.debug = Debug | Info | Off
+
 (** Pre-created hint databases *)
 
 type 'a hint_ast =
@@ -216,7 +218,7 @@ val extern_intern_tac :
    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 -> Pretyping.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 291bc0965..c7567dee0 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -497,8 +497,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/tacticals.ml b/tactics/tacticals.ml
index 203d97542..2a024aa56 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -479,10 +479,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 +533,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.Pretyping.delayed env sigma in
       tclWITHHOLES check (tac x) (Sigma.to_evar_map sigma)
     end }
 
diff --git a/toplevel/metasyntax.mli b/toplevel/metasyntax.mli
index 085cc87c8..f978ec352 100644
--- a/toplevel/metasyntax.mli
+++ b/toplevel/metasyntax.mli
@@ -7,7 +7,6 @@
 (************************************************************************)
 
 open Names
-open Tacexpr
 open Vernacexpr
 open Notation
 open Constrexpr
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 56ddd4d3c..c1142c7cb 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -848,9 +848,7 @@ let vernac_set_end_tac tac =
   let tac = Genarg.out_gen (Genarg.rawwit Constrarg.wit_ltac) tac in
   if not (refining ()) then
     error "Unknown command of the non proof-editing mode.";
-  match tac with
-  | Tacexpr.TacId [] -> ()
-  | _ -> set_end_tac tac
+  set_end_tac tac
     (* TO DO verifier s'il faut pas mettre exist s | TacId s ici*)
 
 let vernac_set_used_variables e =
diff --git a/toplevel/vernacentries.mli b/toplevel/vernacentries.mli
index 4e7fa4a08..7cdc8dd06 100644
--- a/toplevel/vernacentries.mli
+++ b/toplevel/vernacentries.mli
@@ -62,5 +62,5 @@ val with_fail : bool -> (unit -> unit) -> unit
 
 val command_focus : unit Proof.focus_kind
 
-val interp_redexp_hook : (Environ.env -> Evd.evar_map -> Tacexpr.raw_red_expr ->
+val interp_redexp_hook : (Environ.env -> Evd.evar_map -> Genredexpr.raw_red_expr ->
   Evd.evar_map * Redexpr.red_expr) Hook.t