aboutsummaryrefslogtreecommitdiff
path: root/tactics
diff options
context:
space:
mode:
Diffstat (limited to 'tactics')
-rw-r--r--tactics/auto.ml12
-rw-r--r--tactics/auto.mli2
-rw-r--r--tactics/btermdn.ml14
-rw-r--r--tactics/btermdn.mli9
-rw-r--r--tactics/class_tactics.ml14
-rw-r--r--tactics/class_tactics.mli4
-rw-r--r--tactics/eauto.ml11
-rw-r--r--tactics/eauto.mli2
-rw-r--r--tactics/equality.ml24
-rw-r--r--tactics/hints.ml56
-rw-r--r--tactics/hints.mli10
-rw-r--r--tactics/tacticals.ml2
-rw-r--r--tactics/tacticals.mli27
-rw-r--r--tactics/tactics.ml14
-rw-r--r--tactics/tactics.mli7
15 files changed, 105 insertions, 103 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 65b2615b6b..81e487b77d 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -45,7 +45,7 @@ let auto_core_unif_flags_of st1 st2 = {
use_metas_eagerly_in_conv_on_closed_terms = false;
use_evars_eagerly_in_conv_on_closed_terms = false;
modulo_delta = st2;
- modulo_delta_types = full_transparent_state;
+ modulo_delta_types = TransparentState.full;
check_applied_meta_types = false;
use_pattern_unification = false;
use_meta_bound_pattern_unification = true;
@@ -59,13 +59,13 @@ let auto_unif_flags_of st1 st2 =
let flags = auto_core_unif_flags_of st1 st2 in {
core_unify_flags = flags;
merge_unify_flags = flags;
- subterm_unify_flags = { flags with modulo_delta = empty_transparent_state };
+ subterm_unify_flags = { flags with modulo_delta = TransparentState.empty };
allow_K_in_toplevel_higher_order_unification = false;
resolve_evars = true
}
let auto_unif_flags =
- auto_unif_flags_of full_transparent_state empty_transparent_state
+ auto_unif_flags_of TransparentState.full TransparentState.empty
(* Try unification with the precompiled clause, then use registered Apply *)
@@ -291,7 +291,7 @@ let flags_of_state st =
auto_unif_flags_of st st
let auto_flags_of_state st =
- auto_unif_flags_of full_transparent_state st
+ auto_unif_flags_of TransparentState.full st
let hintmap_of sigma secvars hdc concl =
match hdc with
@@ -358,12 +358,12 @@ and my_find_search_delta sigma db_list local_db secvars hdc concl =
let flags = flags_of_state (Hint_db.transparent_state db) in
List.map (fun x -> (Some flags, x)) (f db)
else
- let (ids, csts as st) = Hint_db.transparent_state db in
+ let st = Hint_db.transparent_state db in
let flags, l =
let l =
match hdc with None -> Hint_db.map_none ~secvars db
| Some hdc ->
- if (Id.Pred.is_empty ids && Cpred.is_empty csts)
+ if TransparentState.is_empty st
then Hint_db.map_auto sigma ~secvars hdc concl db
else Hint_db.map_existential sigma ~secvars hdc concl db
in auto_flags_of_state st, l
diff --git a/tactics/auto.mli b/tactics/auto.mli
index a835c1ed95..72d2292ffb 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -22,7 +22,7 @@ val compute_secvars : Proofview.Goal.t -> Id.Pred.t
val default_search_depth : int ref
-val auto_flags_of_state : transparent_state -> Unification.unify_flags
+val auto_flags_of_state : TransparentState.t -> Unification.unify_flags
val connect_hint_clenv : polymorphic -> raw_hint -> clausenv ->
Proofview.Goal.t -> clausenv * constr
diff --git a/tactics/btermdn.ml b/tactics/btermdn.ml
index bfee0422e7..2f2bd8d2bc 100644
--- a/tactics/btermdn.ml
+++ b/tactics/btermdn.ml
@@ -69,13 +69,13 @@ let constr_pat_discr t =
| PRef ((VarRef v) as ref), args -> Some(GRLabel ref,args)
| _ -> None
-let constr_val_discr_st sigma (idpred,cpred) t =
+let constr_val_discr_st sigma ts t =
let c, l = decomp sigma t in
match EConstr.kind sigma c with
- | Const (c,u) -> if Cpred.mem c cpred then Everything else Label(GRLabel (ConstRef c),l)
+ | Const (c,u) -> if TransparentState.is_transparent_constant ts c then Everything else Label(GRLabel (ConstRef c),l)
| Ind (ind_sp,u) -> Label(GRLabel (IndRef ind_sp),l)
| Construct (cstr_sp,u) -> Label(GRLabel (ConstructRef cstr_sp),l)
- | Var id when not (Id.Pred.mem id idpred) -> Label(GRLabel (VarRef id),l)
+ | Var id when not (TransparentState.is_transparent_variable ts id) -> Label(GRLabel (VarRef id),l)
| Prod (n, d, c) -> Label(ProdLabel, [d; c])
| Lambda (n, d, c) ->
if List.is_empty l then
@@ -85,15 +85,15 @@ let constr_val_discr_st sigma (idpred,cpred) t =
| Evar _ -> Everything
| _ -> Nothing
-let constr_pat_discr_st (idpred,cpred) t =
+let constr_pat_discr_st ts t =
match decomp_pat t with
| PRef ((IndRef _) as ref), args
| PRef ((ConstructRef _ ) as ref), args -> Some (GRLabel ref,args)
- | PRef ((VarRef v) as ref), args when not (Id.Pred.mem v idpred) ->
+ | PRef ((VarRef v) as ref), args when not (TransparentState.is_transparent_variable ts v) ->
Some(GRLabel ref,args)
- | PVar v, args when not (Id.Pred.mem v idpred) ->
+ | PVar v, args when not (TransparentState.is_transparent_variable ts v) ->
Some(GRLabel (VarRef v),args)
- | PRef ((ConstRef c) as ref), args when not (Cpred.mem c cpred) ->
+ | PRef ((ConstRef c) as ref), args when not (TransparentState.is_transparent_constant ts c) ->
Some (GRLabel ref, args)
| PProd (_, d, c), [] -> Some (ProdLabel, [d ; c])
| PLambda (_, d, c), [] -> Some (LambdaLabel, [d ; c])
diff --git a/tactics/btermdn.mli b/tactics/btermdn.mli
index 861c9b6250..cc31fb0599 100644
--- a/tactics/btermdn.mli
+++ b/tactics/btermdn.mli
@@ -9,7 +9,6 @@
(************************************************************************)
open Pattern
-open Names
(** Discrimination nets with bounded depth. *)
@@ -19,7 +18,7 @@ open Names
order in such a way patterns having the same prefix have this common
prefix shared and the seek for the action associated to the patterns
that a term matches are found in time proportional to the maximal
-number of nodes of the patterns matching the term. The [transparent_state]
+number of nodes of the patterns matching the term. The [TransparentState.t]
indicates which constants and variables can be considered as rigid.
These dnets are able to cope with existential variables as well, which match
[Everything]. *)
@@ -31,10 +30,10 @@ sig
val empty : t
- val add : transparent_state option -> t -> (constr_pattern * Z.t) -> t
- val rmv : transparent_state option -> t -> (constr_pattern * Z.t) -> t
+ val add : TransparentState.t option -> t -> (constr_pattern * Z.t) -> t
+ val rmv : TransparentState.t option -> t -> (constr_pattern * Z.t) -> t
- val lookup : Evd.evar_map -> transparent_state option -> t -> EConstr.constr -> Z.t list
+ val lookup : Evd.evar_map -> TransparentState.t option -> t -> EConstr.constr -> Z.t list
val app : (Z.t -> unit) -> t -> unit
end
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 81cf9289d1..5959dd54b1 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -358,7 +358,7 @@ let rec e_trivial_fail_db only_classes db_list local_db secvars =
Eauto.registered_e_assumption ::
(tclTHEN Tactics.intro trivial_fail :: [trivial_resolve])
in
- tclFIRST (List.map tclCOMPLETE tacl)
+ tclSOLVE tacl
and e_my_find_search db_list local_db secvars hdc complete only_classes env sigma concl =
let open Proofview.Notations in
@@ -585,9 +585,9 @@ module Search = struct
(** Local hints *)
let autogoal_cache = Summary.ref ~name:"autogoal_cache"
(DirPath.empty, true, Context.Named.empty,
- Hint_db.empty full_transparent_state true)
+ Hint_db.empty TransparentState.full true)
- let make_autogoal_hints only_classes ?(st=full_transparent_state) g =
+ let make_autogoal_hints only_classes ?(st=TransparentState.full) g =
let open Proofview in
let open Tacmach.New in
let sign = Goal.hyps g in
@@ -605,7 +605,7 @@ module Search = struct
in
autogoal_cache := (cwd, only_classes, sign, hints); hints
- let make_autogoal ?(st=full_transparent_state) only_classes dep cut i g =
+ let make_autogoal ?(st=TransparentState.full) only_classes dep cut i g =
let hints = make_autogoal_hints only_classes ~st g in
{ search_hints = hints;
search_depth = [i]; last_tac = lazy (str"none");
@@ -843,7 +843,7 @@ module Search = struct
let info = make_autogoal ?st only_classes dep (cut_of_hints hints) i gl in
search_tac hints depth 1 info
- let search_tac ?(st=full_transparent_state) only_classes dep hints depth =
+ let search_tac ?(st=TransparentState.full) only_classes dep hints depth =
let open Proofview in
let tac sigma gls i =
Goal.enter
@@ -873,7 +873,7 @@ module Search = struct
| (e,ie) -> Proofview.tclZERO ~info:ie e)
in aux 1
- let eauto_tac ?(st=full_transparent_state) ?(unique=false)
+ let eauto_tac ?(st=TransparentState.full) ?(unique=false)
~only_classes ?strategy ~depth ~dep hints =
let open Proofview in
let tac =
@@ -985,7 +985,7 @@ end
(** Binding to either V85 or Search implementations. *)
-let typeclasses_eauto ?(only_classes=false) ?(st=full_transparent_state)
+let typeclasses_eauto ?(only_classes=false) ?(st=TransparentState.full)
?strategy ~depth dbs =
let dbs = List.map_filter
(fun db -> try Some (searchtable_map db)
diff --git a/tactics/class_tactics.mli b/tactics/class_tactics.mli
index 9ba69a0584..46dff34f89 100644
--- a/tactics/class_tactics.mli
+++ b/tactics/class_tactics.mli
@@ -25,7 +25,7 @@ type search_strategy = Dfs | Bfs
val set_typeclasses_strategy : search_strategy -> unit
-val typeclasses_eauto : ?only_classes:bool -> ?st:transparent_state -> ?strategy:search_strategy ->
+val typeclasses_eauto : ?only_classes:bool -> ?st:TransparentState.t -> ?strategy:search_strategy ->
depth:(Int.t option) ->
Hints.hint_db_name list -> unit Proofview.tactic
@@ -39,7 +39,7 @@ val autoapply : constr -> Hints.hint_db_name -> unit Proofview.tactic
module Search : sig
val eauto_tac :
- ?st:Names.transparent_state ->
+ ?st:TransparentState.t ->
(** The transparent_state used when working with local hypotheses *)
?unique:bool ->
(** Should we force a unique solution *)
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index 5067315d08..b8adb792e8 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -15,7 +15,6 @@ open Names
open Constr
open Termops
open EConstr
-open Proof_type
open Tacticals
open Tacmach
open Evd
@@ -29,7 +28,7 @@ open Locusops
open Hints
open Proofview.Notations
-let eauto_unif_flags = auto_flags_of_state full_transparent_state
+let eauto_unif_flags = auto_flags_of_state TransparentState.full
let e_give_exact ?(flags=eauto_unif_flags) c =
Proofview.Goal.enter begin fun gl ->
@@ -151,7 +150,7 @@ let rec e_trivial_fail_db db_list local_db =
(Tacticals.New.tclTHEN Tactics.intro next) ::
(List.map fst (e_trivial_resolve (Tacmach.New.pf_env gl) (Tacmach.New.project gl) db_list local_db secvars (Tacmach.New.pf_concl gl)))
in
- Tacticals.New.tclFIRST (List.map Tacticals.New.tclCOMPLETE tacl)
+ Tacticals.New.tclSOLVE tacl
end
and e_my_find_search env sigma db_list local_db secvars hdc concl =
@@ -203,7 +202,7 @@ let find_first_goal gls =
type search_state = {
priority : int;
depth : int; (*r depth of search before failing *)
- tacres : goal list sigma;
+ tacres : Goal.goal list sigma;
last_tactic : Pp.t Lazy.t;
dblist : hint_db list;
localdb : hint_db list;
@@ -307,7 +306,7 @@ module SearchProblem = struct
let gls = {Evd.it = gl; sigma = lgls.Evd.sigma } in
let hyps' = pf_hyps gls in
if hyps' == hyps then List.hd s.localdb
- else make_local_hint_db (pf_env gls) (project gls) ~ts:full_transparent_state true s.local_lemmas)
+ else make_local_hint_db (pf_env gls) (project gls) ~ts:TransparentState.full true s.local_lemmas)
(List.firstn ((nbgl'-nbgl) + 1) (sig_it lgls))
in
{ depth = pred s.depth; priority = cost; tacres = lgls;
@@ -388,7 +387,7 @@ let make_initial_state dbg n gl dblist localdb lems =
}
let e_search_auto debug (in_depth,p) lems db_list gl =
- let local_db = make_local_hint_db (pf_env gl) (project gl) ~ts:full_transparent_state true lems in
+ let local_db = make_local_hint_db (pf_env gl) (project gl) ~ts:TransparentState.full true lems in
let d = mk_eauto_dbg debug in
let tac = match in_depth,d with
| (true,Debug) -> Search.debug_depth_first
diff --git a/tactics/eauto.mli b/tactics/eauto.mli
index e161d88824..5aa2f42de1 100644
--- a/tactics/eauto.mli
+++ b/tactics/eauto.mli
@@ -26,7 +26,7 @@ val gen_eauto : ?debug:debug -> bool * int -> delayed_open_constr list ->
val eauto_with_bases :
?debug:debug ->
bool * int ->
- delayed_open_constr list -> hint_db list -> Proof_type.tactic
+ delayed_open_constr list -> hint_db list -> Proofview.V82.tac
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/equality.ml b/tactics/equality.ml
index c4a6b1605d..b8967775bf 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -101,8 +101,8 @@ let rewrite_core_unif_flags = {
modulo_conv_on_closed_terms = None;
use_metas_eagerly_in_conv_on_closed_terms = true;
use_evars_eagerly_in_conv_on_closed_terms = false;
- modulo_delta = empty_transparent_state;
- modulo_delta_types = empty_transparent_state;
+ modulo_delta = TransparentState.empty;
+ modulo_delta_types = TransparentState.empty;
check_applied_meta_types = true;
use_pattern_unification = true;
use_meta_bound_pattern_unification = true;
@@ -169,7 +169,7 @@ let instantiate_lemma gl c ty l l2r concl =
[eqclause]
let rewrite_conv_closed_core_unif_flags = {
- modulo_conv_on_closed_terms = Some full_transparent_state;
+ modulo_conv_on_closed_terms = Some TransparentState.full;
(* We have this flag for historical reasons, it has e.g. the consequence *)
(* to rewrite "?x+2" in "y+(1+1)=0" or to rewrite "?x+?x" in "2+(1+1)=0" *)
@@ -178,8 +178,8 @@ let rewrite_conv_closed_core_unif_flags = {
(* Combined with modulo_conv_on_closed_terms, this flag allows since 8.2 *)
(* to rewrite e.g. "?x+(2+?x)" in "1+(1+2)=0" *)
- modulo_delta = empty_transparent_state;
- modulo_delta_types = full_transparent_state;
+ modulo_delta = TransparentState.empty;
+ modulo_delta_types = TransparentState.full;
check_applied_meta_types = true;
use_pattern_unification = true;
(* To rewrite "?n x y" in "y+x=0" when ?n is *)
@@ -204,7 +204,7 @@ let rewrite_conv_closed_unif_flags = {
}
let rewrite_keyed_core_unif_flags = {
- modulo_conv_on_closed_terms = Some full_transparent_state;
+ modulo_conv_on_closed_terms = Some TransparentState.full;
(* We have this flag for historical reasons, it has e.g. the consequence *)
(* to rewrite "?x+2" in "y+(1+1)=0" or to rewrite "?x+?x" in "2+(1+1)=0" *)
@@ -213,8 +213,8 @@ let rewrite_keyed_core_unif_flags = {
(* Combined with modulo_conv_on_closed_terms, this flag allows since 8.2 *)
(* to rewrite e.g. "?x+(2+?x)" in "1+(1+2)=0" *)
- modulo_delta = full_transparent_state;
- modulo_delta_types = full_transparent_state;
+ modulo_delta = TransparentState.full;
+ modulo_delta_types = TransparentState.full;
check_applied_meta_types = true;
use_pattern_unification = true;
(* To rewrite "?n x y" in "y+x=0" when ?n is *)
@@ -1028,7 +1028,7 @@ let discr_positions env sigma (lbeq,eqn,(t,t1,t2)) eq_clause cpath dirn =
let absurd_clause = apply_on_clause (pf,pf_ty) eq_clause in
let pf = Clenvtac.clenv_value_cast_meta absurd_clause in
tclTHENS (assert_after Anonymous absurd_term)
- [onLastHypId gen_absurdity; (Proofview.V82.tactic (Tacmach.refine pf))]
+ [onLastHypId gen_absurdity; (Proofview.V82.tactic (Refiner.refiner ~check:true EConstr.Unsafe.(to_constr pf)))]
let discrEq (lbeq,_,(t,t1,t2) as u) eq_clause =
let sigma = eq_clause.evd in
@@ -1354,8 +1354,8 @@ let inject_if_homogenous_dependent_pair ty =
tclTHENS (cut (mkApp (ceq,new_eq_args)))
[clear [destVar sigma hyp];
Tacticals.New.pf_constr_of_global inj2 >>= fun inj2 ->
- Proofview.V82.tactic (Tacmach.refine
- (mkApp(inj2,[|ar1.(0);mkConst c;ar1.(1);ar1.(2);ar1.(3);ar2.(3);hyp|])))
+ Proofview.V82.tactic (Refiner.refiner ~check:true EConstr.Unsafe.(to_constr
+ (mkApp(inj2,[|ar1.(0);mkConst c;ar1.(1);ar1.(2);ar1.(3);ar2.(3);hyp|]))))
])]
with Exit ->
Proofview.tclUNIT ()
@@ -1400,7 +1400,7 @@ let inject_at_positions env sigma l2r (eq,_,(t,t1,t2)) eq_clause posns tac =
(Proofview.tclIGNORE (Proofview.Monad.List.map
(fun (pf,ty) -> tclTHENS (cut ty)
[inject_if_homogenous_dependent_pair ty;
- Proofview.V82.tactic (Tacmach.refine pf)])
+ Proofview.V82.tactic (Refiner.refiner ~check:true EConstr.Unsafe.(to_constr pf))])
(if l2r then List.rev injectors else injectors)))
(tac (List.length injectors)))
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 2f2d32e887..e64e08dbde 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -290,9 +290,9 @@ let lookup_tacs sigma concl st se =
module Constr_map = Map.Make(GlobRef.Ordered)
-let is_transparent_gr (ids, csts) = function
- | VarRef id -> Id.Pred.mem id ids
- | ConstRef cst -> Cpred.mem cst csts
+let is_transparent_gr ts = function
+ | VarRef id -> TransparentState.is_transparent_variable ts id
+ | ConstRef cst -> TransparentState.is_transparent_constant ts cst
| IndRef _ | ConstructRef _ -> false
let strip_params env sigma c =
@@ -497,7 +497,7 @@ type hint_db_name = string
module Hint_db :
sig
type t
-val empty : ?name:hint_db_name -> transparent_state -> bool -> t
+val empty : ?name:hint_db_name -> TransparentState.t -> bool -> t
val find : GlobRef.t -> t -> search_entry
val map_none : secvars:Id.Pred.t -> t -> full_hint list
val map_all : secvars:Id.Pred.t -> GlobRef.t -> t -> full_hint list
@@ -513,8 +513,8 @@ val remove_one : GlobRef.t -> t -> t
val remove_list : GlobRef.t list -> t -> t
val iter : (GlobRef.t option -> hint_mode array list -> full_hint list -> unit) -> t -> unit
val use_dn : t -> bool
-val transparent_state : t -> transparent_state
-val set_transparent_state : t -> transparent_state -> t
+val transparent_state : t -> TransparentState.t
+val set_transparent_state : t -> TransparentState.t -> t
val add_cut : hints_path -> t -> t
val add_mode : GlobRef.t -> hint_mode array -> t -> t
val cut : t -> hints_path
@@ -526,7 +526,7 @@ end =
struct
type t = {
- hintdb_state : Names.transparent_state;
+ hintdb_state : TransparentState.t;
hintdb_cut : hints_path;
hintdb_unfolds : Id.Set.t * Cset.t;
hintdb_max_id : int;
@@ -663,10 +663,13 @@ struct
let st',db,rebuild =
match v.code.obj with
| Unfold_nth egr ->
- let addunf (ids,csts) (ids',csts') =
+ let addunf ts (ids, csts) =
+ let open TransparentState in
match egr with
- | EvalVarRef id -> (Id.Pred.add id ids, csts), (Id.Set.add id ids', csts')
- | EvalConstRef cst -> (ids, Cpred.add cst csts), (ids', Cset.add cst csts')
+ | EvalVarRef id ->
+ { ts with tr_var = Id.Pred.add id ts.tr_var }, (Id.Set.add id ids, csts)
+ | EvalConstRef cst ->
+ { ts with tr_cst = Cpred.add cst ts.tr_cst }, (ids, Cset.add cst csts)
in
let state, unfs = addunf db.hintdb_state db.hintdb_unfolds in
state, { db with hintdb_unfolds = unfs }, true
@@ -740,8 +743,8 @@ let typeclasses_db = "typeclass_instances"
let rewrite_db = "rewrite"
let auto_init_db =
- Hintdbmap.add typeclasses_db (Hint_db.empty full_transparent_state true)
- (Hintdbmap.add rewrite_db (Hint_db.empty cst_full_transparent_state true)
+ Hintdbmap.add typeclasses_db (Hint_db.empty TransparentState.full true)
+ (Hintdbmap.add rewrite_db (Hint_db.empty TransparentState.cst_full true)
Hintdbmap.empty)
let searchtable = Summary.ref ~name:"searchtable" auto_init_db
@@ -977,7 +980,7 @@ let make_trivial env sigma poly ?(name=PathAny) r =
let get_db dbname =
try searchtable_map dbname
- with Not_found -> Hint_db.empty ~name:dbname empty_transparent_state false
+ with Not_found -> Hint_db.empty ~name:dbname TransparentState.empty false
let add_hint dbname hintlist =
let check (_, h) =
@@ -995,18 +998,19 @@ let add_hint dbname hintlist =
searchtable_add (dbname,db')
let add_transparency dbname target b =
+ let open TransparentState in
let db = get_db dbname in
- let (ids, csts as st) = Hint_db.transparent_state db in
+ let st = Hint_db.transparent_state db in
let st' =
match target with
- | HintsVariables -> (if b then Id.Pred.full else Id.Pred.empty), csts
- | HintsConstants -> ids, if b then Cpred.full else Cpred.empty
+ | HintsVariables -> { st with tr_var = (if b then Id.Pred.full else Id.Pred.empty) }
+ | HintsConstants -> { st with tr_cst = (if b then Cpred.full else Cpred.empty) }
| HintsReferences grs ->
- List.fold_left (fun (ids, csts) gr ->
- match gr with
- | EvalConstRef c -> (ids, (if b then Cpred.add else Cpred.remove) c csts)
- | EvalVarRef v -> (if b then Id.Pred.add else Id.Pred.remove) v ids, csts)
- st grs
+ List.fold_left (fun st gr ->
+ match gr with
+ | EvalConstRef c -> { st with tr_cst = (if b then Cpred.add else Cpred.remove) c st.tr_cst }
+ | EvalVarRef v -> { st with tr_var = (if b then Id.Pred.add else Id.Pred.remove) v st.tr_var })
+ st grs
in searchtable_add (dbname, Hint_db.set_transparent_state db st')
let remove_hint dbname grs =
@@ -1015,7 +1019,7 @@ let remove_hint dbname grs =
searchtable_add (dbname, db')
type hint_action =
- | CreateDB of bool * transparent_state
+ | CreateDB of bool * TransparentState.t
| AddTransparency of evaluable_global_reference hints_transparency_target * bool
| AddHints of hint_entry list
| RemoveHints of GlobRef.t list
@@ -1373,10 +1377,10 @@ let interp_hints poly =
let _, tacexp = Genintern.generic_intern env tacexp in
HintsExternEntry ({ hint_priority = Some pri; hint_pattern = pat }, tacexp)
-let add_hints ~local dbnames0 h =
- if String.List.mem "nocore" dbnames0 then
+let add_hints ~local dbnames h =
+ if String.List.mem "nocore" dbnames then
user_err Pp.(str "The hint database \"nocore\" is meant to stay empty.");
- let dbnames = if List.is_empty dbnames0 then ["core"] else dbnames0 in
+ assert (not (List.is_empty dbnames));
let env = Global.env() in
let sigma = Evd.from_env env in
match h with
@@ -1543,7 +1547,7 @@ let pr_hint_db_env env sigma db =
in
Hint_db.fold fold db (mt ())
in
- let (ids, csts) = Hint_db.transparent_state db in
+ let { TransparentState.tr_var = ids; tr_cst = csts } = Hint_db.transparent_state db in
hov 0
((if Hint_db.use_dn db then str"Discriminated database"
else str"Non-discriminated database")) ++ fnl () ++
diff --git a/tactics/hints.mli b/tactics/hints.mli
index 6db8feccd0..dd2c63d351 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -122,7 +122,7 @@ val glob_hints_path :
module Hint_db :
sig
type t
- val empty : ?name:hint_db_name -> transparent_state -> bool -> t
+ val empty : ?name:hint_db_name -> TransparentState.t -> bool -> t
val find : GlobRef.t -> t -> search_entry
(** All hints which have no pattern.
@@ -155,8 +155,8 @@ module Hint_db :
hint_mode array list -> full_hint list -> unit) -> t -> unit
val use_dn : t -> bool
- val transparent_state : t -> transparent_state
- val set_transparent_state : t -> transparent_state -> t
+ val transparent_state : t -> TransparentState.t
+ val set_transparent_state : t -> TransparentState.t -> t
val add_cut : hints_path -> t -> t
val cut : t -> hints_path
@@ -191,7 +191,7 @@ val searchtable_add : (hint_db_name * hint_db) -> unit
[use_dn] switches the use of the discrimination net for all hints
and patterns. *)
-val create_hint_db : bool -> hint_db_name -> transparent_state -> bool -> unit
+val create_hint_db : bool -> hint_db_name -> TransparentState.t -> bool -> unit
val remove_hints : bool -> hint_db_name list -> GlobRef.t list -> unit
@@ -273,7 +273,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 -> delayed_open_constr list -> hint_db
+val make_local_hint_db : env -> evar_map -> ?ts:TransparentState.t -> bool -> delayed_open_constr list -> hint_db
val make_db_list : hint_db_name list -> hint_db list
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index f2cf915fe3..224cd68cf9 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -26,6 +26,8 @@ module NamedDecl = Context.Named.Declaration
(* Tacticals re-exported from the Refiner module *)
(************************************************************************)
+type tactic = Proofview.V82.tac
+
let tclIDTAC = Refiner.tclIDTAC
let tclIDTAC_MESSAGE = Refiner.tclIDTAC_MESSAGE
let tclORELSE0 = Refiner.tclORELSE0
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index cc15469d0e..2947e44f7a 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -12,12 +12,13 @@ open Names
open Constr
open EConstr
open Evd
-open Proof_type
open Locus
open Tactypes
(** Tacticals i.e. functions from tactics to tactics. *)
+type tactic = Proofview.V82.tac
+
val tclIDTAC : tactic
val tclIDTAC_MESSAGE : Pp.t -> tactic
val tclORELSE0 : tactic -> tactic -> tactic
@@ -65,20 +66,20 @@ val onNLastHypsId : int -> (Id.t list -> tactic) -> tactic
val onNLastHyps : int -> (constr list -> tactic) -> tactic
val onNLastDecls : int -> (named_context -> tactic) -> tactic
-val lastHypId : goal sigma -> Id.t
-val lastHyp : goal sigma -> constr
-val lastDecl : goal sigma -> named_declaration
-val nLastHypsId : int -> goal sigma -> Id.t list
-val nLastHyps : int -> goal sigma -> constr list
-val nLastDecls : int -> goal sigma -> named_context
+val lastHypId : Goal.goal sigma -> Id.t
+val lastHyp : Goal.goal sigma -> constr
+val lastDecl : Goal.goal sigma -> named_declaration
+val nLastHypsId : int -> Goal.goal sigma -> Id.t list
+val nLastHyps : int -> Goal.goal sigma -> constr list
+val nLastDecls : int -> Goal.goal sigma -> named_context
-val afterHyp : Id.t -> goal sigma -> named_context
+val afterHyp : Id.t -> Goal.goal sigma -> named_context
val ifOnHyp : (Id.t * types -> bool) ->
(Id.t -> tactic) -> (Id.t -> tactic) ->
Id.t -> tactic
-val onHyps : (goal sigma -> named_context) ->
+val onHyps : (Goal.goal sigma -> named_context) ->
(named_context -> tactic) -> tactic
(** {6 Tacticals applying to goal components } *)
@@ -127,11 +128,11 @@ val compute_constructor_signatures : rec_flag:bool -> inductive * 'a -> bool lis
val compute_induction_names :
bool list array -> or_and_intro_pattern option -> intro_patterns array
-val elimination_sort_of_goal : goal sigma -> Sorts.family
-val elimination_sort_of_hyp : Id.t -> goal sigma -> Sorts.family
-val elimination_sort_of_clause : Id.t option -> goal sigma -> Sorts.family
+val elimination_sort_of_goal : Goal.goal sigma -> Sorts.family
+val elimination_sort_of_hyp : Id.t -> Goal.goal sigma -> Sorts.family
+val elimination_sort_of_clause : Id.t option -> Goal.goal sigma -> Sorts.family
-val pf_with_evars : (goal sigma -> Evd.evar_map * 'a) -> ('a -> tactic) -> tactic
+val pf_with_evars : (Goal.goal sigma -> Evd.evar_map * 'a) -> ('a -> tactic) -> tactic
val pf_constr_of_global : GlobRef.t -> (constr -> tactic) -> tactic
(** Tacticals defined directly in term of Proofview *)
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 1646906daa..0beafb7e31 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -142,7 +142,6 @@ let introduction id =
| _ -> raise (RefinerError (env, sigma, IntroNeedsProduct))
end
-let refine = Tacmach.refine
let error msg = CErrors.user_err Pp.(str msg)
let convert_concl ?(check=true) ty k =
@@ -1152,7 +1151,6 @@ let rec intros_move = function
let tactic_infer_flags with_evar = {
Pretyping.use_typeclasses = true;
Pretyping.solve_unification_constraints = true;
- Pretyping.use_hook = Pfedit.solve_by_implicit_tactic ();
Pretyping.fail_evar = not with_evar;
Pretyping.expand_evars = true }
@@ -1301,7 +1299,7 @@ let clenv_refine_in ?(sidecond_first=false) with_evars ?(with_classes=true)
if not with_evars && occur_meta clenv.evd new_hyp_typ then
error_uninstantiated_metas new_hyp_typ clenv;
let new_hyp_prf = clenv_value clenv in
- let exact_tac = Proofview.V82.tactic (Tacmach.refine_no_check new_hyp_prf) in
+ let exact_tac = Proofview.V82.tactic (Refiner.refiner ~check:false EConstr.Unsafe.(to_constr new_hyp_prf)) in
let naming = NamingMustBe (CAst.make targetid) in
let with_clear = do_replace (Some id) naming in
Tacticals.New.tclTHEN
@@ -1625,7 +1623,7 @@ let descend_in_conjunctions avoid tac (err, info) c =
| Some (p,pt) ->
Tacticals.New.tclTHENS
(assert_before_gen false (NamingAvoid avoid) pt)
- [Proofview.V82.tactic (refine p);
+ [Proofview.V82.tactic (refiner ~check:true EConstr.Unsafe.(to_constr p));
(* Might be ill-typed due to forbidden elimination. *)
Tacticals.New.onLastHypId (tac (not isrec))]
end)))
@@ -1661,7 +1659,7 @@ let general_apply ?(respect_opaque=false) with_delta with_destruct with_evars
let sigma = Tacmach.New.project gl in
let ts =
if respect_opaque then Conv_oracle.get_transp_state (oracle env)
- else full_transparent_state
+ else TransparentState.full
in
let flags =
if with_delta then default_unify_flags () else default_no_delta_unify_flags ts in
@@ -1827,7 +1825,7 @@ let apply_in_once ?(respect_opaque = false) sidecond_first with_delta
let sigma = Tacmach.New.project gl in
let ts =
if respect_opaque then Conv_oracle.get_transp_state (oracle env)
- else full_transparent_state
+ else TransparentState.full
in
let flags =
if with_delta then default_unify_flags () else default_no_delta_unify_flags ts in
@@ -4910,7 +4908,7 @@ let constr_eq ~strict x y =
| None -> fail
end
-let unify ?(state=full_transparent_state) x y =
+let unify ?(state=TransparentState.full) x y =
Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Proofview.Goal.sigma gl in
@@ -4923,7 +4921,7 @@ let unify ?(state=full_transparent_state) x y =
let flags = { (default_unify_flags ()) with
core_unify_flags = core_flags;
merge_unify_flags = core_flags;
- subterm_unify_flags = { core_flags with modulo_delta = empty_transparent_state } }
+ subterm_unify_flags = { core_flags with modulo_delta = TransparentState.empty } }
in
let sigma = w_unify (Tacmach.New.pf_env gl) sigma Reduction.CONV ~flags x y in
Proofview.Unsafe.tclEVARS sigma
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index b298524ff8..75b5caaa36 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -12,7 +12,6 @@ open Names
open Constr
open EConstr
open Environ
-open Proof_type
open Evd
open Clenv
open Redexpr
@@ -50,8 +49,8 @@ val convert_leq : constr -> constr -> unit Proofview.tactic
(** {6 Introduction tactics. } *)
val fresh_id_in_env : Id.Set.t -> Id.t -> env -> Id.t
-val fresh_id : Id.Set.t -> Id.t -> goal sigma -> Id.t
-val find_intro_names : rel_context -> goal sigma -> Id.t list
+val fresh_id : Id.Set.t -> Id.t -> Goal.goal sigma -> Id.t
+val find_intro_names : rel_context -> Goal.goal sigma -> Id.t list
val intro : unit Proofview.tactic
val introf : unit Proofview.tactic
@@ -419,7 +418,7 @@ val generalize_dep : ?with_let:bool (** Don't lose let bindings *) -> constr -
are added to the evar map. *)
val constr_eq : strict:bool -> constr -> constr -> unit Proofview.tactic
-val unify : ?state:Names.transparent_state -> constr -> constr -> unit Proofview.tactic
+val unify : ?state:TransparentState.t -> constr -> constr -> unit Proofview.tactic
val abstract_generalize : ?generalize_vars:bool -> ?force_dep:bool -> Id.t -> unit Proofview.tactic
val specialize_eqs : Id.t -> unit Proofview.tactic
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 14:21:14 +0000