aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
diff options
context:
space:
mode:
Diffstat (limited to 'tactics')
-rw-r--r--tactics/auto.ml1
-rw-r--r--tactics/auto.mli40
-rw-r--r--tactics/autorewrite.mli1
-rw-r--r--tactics/eauto.ml3
-rw-r--r--tactics/eauto.mli8
-rw-r--r--tactics/elim.mli2
-rw-r--r--tactics/hints.ml7
-rw-r--r--tactics/hints.mli4
-rw-r--r--tactics/inv.ml2
-rw-r--r--tactics/tacticals.ml10
10 files changed, 38 insertions, 40 deletions
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 }
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-23 18:41:46 +0000