aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--intf/misctypes.mli9
-rw-r--r--intf/tacexpr.mli2
-rw-r--r--lib/future.mli2
-rw-r--r--pretyping/constr_matching.ml1
-rw-r--r--pretyping/constr_matching.mli6
-rw-r--r--pretyping/pretyping.ml1
-rw-r--r--pretyping/pretyping.mli2
-rw-r--r--proofs/clenvtac.mli2
-rw-r--r--proofs/proof_type.mli1
-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
-rw-r--r--toplevel/metasyntax.mli1
-rw-r--r--toplevel/vernacentries.ml4
-rw-r--r--toplevel/vernacentries.mli2
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
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-01 06:41:52 +0000