aboutsummaryrefslogtreecommitdiff
path: root/tactics
diff options
context:
space:
mode:
Diffstat (limited to 'tactics')
-rw-r--r--tactics/autorewrite.ml2
-rw-r--r--tactics/btermdn.ml2
-rw-r--r--tactics/class_tactics.ml2
-rw-r--r--tactics/equality.ml2
-rw-r--r--tactics/hints.ml27
-rw-r--r--tactics/hints.mli3
-rw-r--r--tactics/tactics.ml30
-rw-r--r--tactics/tactics.mli2
-rw-r--r--tactics/term_dnet.ml2
9 files changed, 39 insertions, 33 deletions
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index c8fd0b7a75..8e296de617 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -162,7 +162,7 @@ let gen_auto_multi_rewrite conds tac_main lbas cl =
| None ->
(* try to rewrite in all hypothesis
(except maybe the rewritten one) *)
- Proofview.Goal.nf_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let ids = Tacmach.New.pf_ids_of_hyps gl in
try_do_hyps (fun id -> id) ids
end)
diff --git a/tactics/btermdn.ml b/tactics/btermdn.ml
index aca7f6c65e..bfee0422e7 100644
--- a/tactics/btermdn.ml
+++ b/tactics/btermdn.ml
@@ -28,7 +28,7 @@ type term_label =
| SortLabel
let compare_term_label t1 t2 = match t1, t2 with
-| GRLabel gr1, GRLabel gr2 -> RefOrdered.compare gr1 gr2
+| GRLabel gr1, GRLabel gr2 -> GlobRef.Ordered.compare gr1 gr2
| _ -> Pervasives.compare t1 t2 (** OK *)
type 'res lookup_res = 'res Dn.lookup_res = Label of 'res | Nothing | Everything
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 9c5fdcd1ce..3456d13bbe 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -416,7 +416,7 @@ and e_my_find_search db_list local_db secvars hdc complete only_classes env sigm
if get_typeclasses_filtered_unification () then
let tac =
matches_pattern concl p <*>
- Proofview.Goal.nf_enter
+ Proofview.Goal.enter
(fun gl -> unify_resolve_refine poly flags gl (c,None,clenv)) in
Tacticals.New.tclTHEN tac Proofview.shelve_unifiable
else
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 0e39215701..d0f4b2c680 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -249,7 +249,7 @@ let rewrite_elim with_evars frzevars cls c e =
let tclNOTSAMEGOAL tac =
let goal gl = Proofview.Goal.goal gl in
- Proofview.Goal.nf_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let sigma = project gl in
let ev = goal gl in
tac >>= fun () ->
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 43a450ea71..3835dee299 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -288,7 +288,7 @@ let lookup_tacs sigma concl st se =
let sl' = List.stable_sort pri_order_int l' in
List.merge pri_order_int se.sentry_nopat sl'
-module Constr_map = Map.Make(RefOrdered)
+module Constr_map = Map.Make(GlobRef.Ordered)
let is_transparent_gr (ids, csts) = function
| VarRef id -> Id.Pred.mem id ids
@@ -734,8 +734,6 @@ module Hintdbmap = String.Map
type hint_db = Hint_db.t
-type hint_db_table = hint_db Hintdbmap.t ref
-
(** Initially created hint databases, for typeclasses and rewrite *)
let typeclasses_db = "typeclass_instances"
@@ -746,8 +744,8 @@ let auto_init_db =
(Hintdbmap.add rewrite_db (Hint_db.empty cst_full_transparent_state true)
Hintdbmap.empty)
-let searchtable : hint_db_table = ref auto_init_db
-let statustable = ref KNmap.empty
+let searchtable = Summary.ref ~name:"searchtable" auto_init_db
+let statustable = Summary.ref ~name:"statustable" KNmap.empty
let searchtable_map name =
Hintdbmap.find name !searchtable
@@ -762,25 +760,6 @@ let error_no_such_hint_database x =
user_err ~hdr:"Hints" (str "No such Hint database: " ++ str x ++ str ".")
(**************************************************************************)
-(* Definition of the summary *)
-(**************************************************************************)
-
-let hints_init : (unit -> unit) ref = ref (fun () -> ())
-let add_hints_init f =
- let init = !hints_init in
- hints_init := (fun () -> init (); f ())
-
-let init () =
- searchtable := auto_init_db; statustable := KNmap.empty; !hints_init ()
-let freeze _ = (!searchtable, !statustable)
-let unfreeze (fs, st) = searchtable := fs; statustable := st
-
-let _ = Summary.declare_summary "search"
- { Summary.freeze_function = freeze;
- Summary.unfreeze_function = unfreeze;
- Summary.init_function = init }
-
-(**************************************************************************)
(* Auxiliary functions to prepare AUTOHINT objects *)
(**************************************************************************)
diff --git a/tactics/hints.mli b/tactics/hints.mli
index 9bf6c175a5..c49ca2094a 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -293,8 +293,5 @@ val pr_hint_db : Hint_db.t -> Pp.t
[@@ocaml.deprecated "please used pr_hint_db_env"]
val pr_hint : env -> evar_map -> hint -> Pp.t
-(** Hook for changing the initialization of auto *)
-val add_hints_init : (unit -> unit) -> unit
-
type nonrec hint_info = hint_info
[@@ocaml.deprecated "Use [Typeclasses.hint_info]"]
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index d536204ec3..6999b17d8e 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -2690,6 +2690,34 @@ let mkletin_goal env sigma store with_eq dep (id,lastlhyp,ccl,c) ty =
let (sigma, x) = new_evar newenv sigma ~principal:true ~store ccl in
(sigma, mkNamedLetIn id c t x)
+let pose_tac na c =
+ Proofview.Goal.enter begin fun gl ->
+ let sigma = Proofview.Goal.sigma gl in
+ let env = Proofview.Goal.env gl in
+ let hyps = named_context_val env in
+ let concl = Proofview.Goal.concl gl in
+ let t = typ_of env sigma c in
+ let (sigma, t) = Evarsolve.refresh_universes ~onlyalg:true (Some false) env sigma t in
+ let id = match na with
+ | Name id ->
+ let () = if mem_named_context_val id hyps then
+ user_err (str "Variable " ++ Id.print id ++ str " is already declared.")
+ in
+ id
+ | Anonymous ->
+ let id = id_of_name_using_hdchar env sigma t Anonymous in
+ next_ident_away_in_goal id (ids_of_named_context_val hyps)
+ in
+ Proofview.Unsafe.tclEVARS sigma <*>
+ Refine.refine ~typecheck:false begin fun sigma ->
+ let nhyps = EConstr.push_named_context_val (NamedDecl.LocalDef (id, c, t)) hyps in
+ let (sigma, ev) = Evarutil.new_pure_evar nhyps sigma concl in
+ let inst = Array.map_of_list (fun d -> mkVar (get_id d)) (named_context env) in
+ let body = mkEvar (ev, Array.append [|mkRel 1|] inst) in
+ (sigma, mkLetIn (Name id, c, t, body))
+ end
+ end
+
let letin_tac with_eq id c ty occs =
Proofview.Goal.enter begin fun gl ->
let sigma = Proofview.Goal.sigma gl in
@@ -2796,7 +2824,7 @@ let generalize_goal gl i ((occs,c,b),na as o) (cl,sigma) =
let generalize_dep ?(with_let=false) c =
let open Tacmach.New in
let open Tacticals.New in
- Proofview.Goal.nf_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let env = pf_env gl in
let sign = Proofview.Goal.hyps gl in
let sigma = project gl in
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 57f20d2ff2..c088e404b0 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -390,6 +390,8 @@ val cut : types -> unit Proofview.tactic
(** {6 Tactics for adding local definitions. } *)
+val pose_tac : Name.t -> constr -> unit Proofview.tactic
+
val letin_tac : (bool * intro_pattern_naming) option ->
Name.t -> constr -> types option -> clause -> unit Proofview.tactic
diff --git a/tactics/term_dnet.ml b/tactics/term_dnet.ml
index 8bdcc63215..03d2a17eee 100644
--- a/tactics/term_dnet.ml
+++ b/tactics/term_dnet.ml
@@ -100,7 +100,7 @@ struct
| DRel, _ -> -1 | _, DRel -> 1
| DSort, DSort -> 0
| DSort, _ -> -1 | _, DSort -> 1
- | DRef gr1, DRef gr2 -> RefOrdered.compare gr1 gr2
+ | DRef gr1, DRef gr2 -> GlobRef.Ordered.compare gr1 gr2
| DRef _, _ -> -1 | _, DRef _ -> 1
| DCtx (tl1, tr1), DCtx (tl2, tr2)
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-01 15:43:55 +0000