aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
diff options
context:
space:
mode:
Diffstat (limited to 'tactics')
-rw-r--r--tactics/auto.ml5
-rw-r--r--tactics/autorewrite.ml4
-rw-r--r--tactics/autorewrite.mli2
-rw-r--r--tactics/class_tactics.ml7
-rw-r--r--tactics/eauto.ml3
-rw-r--r--tactics/hints.ml70
-rw-r--r--tactics/hints.mli11
-rw-r--r--tactics/inv.ml3
-rw-r--r--tactics/leminv.ml2
-rw-r--r--tactics/tactics.ml20
10 files changed, 72 insertions, 55 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml
index d0424eb89..fa8435d1f 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -388,7 +388,7 @@ and tac_of_hint dbg db_list local_db concl (flags, ({pat=p; code=t;poly=poly;db=
Tacticals.New.tclPROGRESS (reduce (Unfold [AllOccurrences,c]) Locusops.onConcl)
else Tacticals.New.tclFAIL 0 (str"Unbound reference")
end
- | Extern tacast ->
+ | Extern tacast ->
conclPattern concl p tacast
in
let pr_hint () =
@@ -396,7 +396,8 @@ and tac_of_hint dbg db_list local_db concl (flags, ({pat=p; code=t;poly=poly;db=
| None -> mt ()
| Some n -> str " (in " ++ str n ++ str ")"
in
- pr_hint t ++ origin
+ let sigma, env = Pfedit.get_current_context () in
+ pr_hint env sigma t ++ origin
in
tclLOG dbg pr_hint (run_hint t tactic)
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index e68087f14..6a9cd7e20 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -74,12 +74,12 @@ let find_matches bas pat =
let res = HintDN.search_pattern base pat in
List.map snd res
-let print_rewrite_hintdb bas =
+let print_rewrite_hintdb env sigma bas =
(str "Database " ++ str bas ++ fnl () ++
prlist_with_sep fnl
(fun h ->
str (if h.rew_l2r then "rewrite -> " else "rewrite <- ") ++
- Printer.pr_lconstr h.rew_lemma ++ str " of type " ++ Printer.pr_lconstr h.rew_type ++
+ Printer.pr_lconstr_env env sigma h.rew_lemma ++ str " of type " ++ Printer.pr_lconstr_env env sigma h.rew_type ++
Option.cata (fun tac -> str " then use tactic " ++
Pputils.pr_glb_generic (Global.env()) tac) (mt ()) h.rew_tac)
(find_rewrites bas))
diff --git a/tactics/autorewrite.mli b/tactics/autorewrite.mli
index d2b5e070b..44acf3c01 100644
--- a/tactics/autorewrite.mli
+++ b/tactics/autorewrite.mli
@@ -40,7 +40,7 @@ val auto_multi_rewrite : ?conds:conditions -> string list -> Locus.clause -> uni
val auto_multi_rewrite_with : ?conds:conditions -> unit Proofview.tactic -> string list -> Locus.clause -> unit Proofview.tactic
-val print_rewrite_hintdb : string -> Pp.t
+val print_rewrite_hintdb : Environ.env -> Evd.evar_map -> string -> Pp.t
open Clenv
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index b98b10315..cee6d4bea 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -464,15 +464,16 @@ and e_my_find_search db_list local_db secvars hdc complete only_classes sigma co
in
let tac = run_hint t tac in
let tac = if complete then Tacticals.New.tclCOMPLETE tac else tac in
+ let _, env = Pfedit.get_current_context () in
let pp =
match p with
| Some pat when get_typeclasses_filtered_unification () ->
- str " with pattern " ++ Printer.pr_constr_pattern pat
+ str " with pattern " ++ Printer.pr_constr_pattern_env env sigma pat
| _ -> mt ()
in
match repr_hint t with
- | Extern _ -> (tac, b, true, name, lazy (pr_hint t ++ pp))
- | _ -> (tac, b, false, name, lazy (pr_hint t ++ pp))
+ | Extern _ -> (tac, b, true, name, lazy (pr_hint env sigma t ++ pp))
+ | _ -> (tac, b, false, name, lazy (pr_hint env sigma t ++ pp))
in List.map tac_of_hint hintl
and e_trivial_resolve db_list local_db secvars only_classes sigma concl =
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index 239661498..f5c6ab879 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -178,7 +178,8 @@ and e_my_find_search sigma db_list local_db secvars hdc concl =
| Extern tacast -> conclPattern concl p tacast
in
let tac = run_hint t tac in
- (tac, lazy (pr_hint t)))
+ let sigma, env = Pfedit.get_current_context () in
+ (tac, lazy (pr_hint env sigma t)))
in
List.map tac_of_hint hintl
diff --git a/tactics/hints.ml b/tactics/hints.ml
index c7c53b393..70e84013b 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -1392,14 +1392,14 @@ let make_db_list dbnames =
(* Functions for printing the hints *)
(**************************************************************************)
-let pr_hint_elt (c, _, _) = pr_econstr c
+let pr_hint_elt env sigma (c, _, _) = pr_econstr_env env sigma c
-let pr_hint h = match h.obj with
- | Res_pf (c, _) -> (str"simple apply " ++ pr_hint_elt c)
- | ERes_pf (c, _) -> (str"simple eapply " ++ pr_hint_elt c)
- | Give_exact (c, _) -> (str"exact " ++ pr_hint_elt c)
+let pr_hint env sigma h = match h.obj with
+ | Res_pf (c, _) -> (str"simple apply " ++ pr_hint_elt env sigma c)
+ | ERes_pf (c, _) -> (str"simple eapply " ++ pr_hint_elt env sigma c)
+ | Give_exact (c, _) -> (str"exact " ++ pr_hint_elt env sigma c)
| Res_pf_THEN_trivial_fail (c, _) ->
- (str"simple apply " ++ pr_hint_elt c ++ str" ; trivial")
+ (str"simple apply " ++ pr_hint_elt env sigma c ++ str" ; trivial")
| Unfold_nth c -> (str"unfold " ++ pr_evaluable_reference c)
| Extern tac ->
let env =
@@ -1410,21 +1410,21 @@ let pr_hint h = match h.obj with
in
(str "(*external*) " ++ Pputils.pr_glb_generic env tac)
-let pr_id_hint (id, v) =
- let pr_pat p = str", pattern " ++ pr_lconstr_pattern p in
- (pr_hint v.code ++ str"(level " ++ int v.pri ++ pr_opt_no_spc pr_pat v.pat
+let pr_id_hint env sigma (id, v) =
+ let pr_pat p = str", pattern " ++ pr_lconstr_pattern_env env sigma p in
+ (pr_hint env sigma v.code ++ str"(level " ++ int v.pri ++ pr_opt_no_spc pr_pat v.pat
++ str", id " ++ int id ++ str ")" ++ spc ())
-let pr_hint_list hintlist =
- (str " " ++ hov 0 (prlist pr_id_hint hintlist) ++ fnl ())
+let pr_hint_list env sigma hintlist =
+ (str " " ++ hov 0 (prlist (pr_id_hint env sigma) hintlist) ++ fnl ())
-let pr_hints_db (name,db,hintlist) =
+let pr_hints_db env sigma (name,db,hintlist) =
(str "In the database " ++ str name ++ str ":" ++
if List.is_empty hintlist then (str " nothing" ++ fnl ())
- else (fnl () ++ pr_hint_list hintlist))
+ else (fnl () ++ pr_hint_list env sigma hintlist))
(* Print all hints associated to head c in any database *)
-let pr_hint_list_for_head c =
+let pr_hint_list_for_head env sigma c =
let dbs = current_db () in
let validate (name, db) =
let hints = List.map (fun v -> 0, v) (Hint_db.map_all ~secvars:Id.Pred.full c db) in
@@ -1436,13 +1436,13 @@ let pr_hint_list_for_head c =
else
hov 0
(str"For " ++ pr_global c ++ str" -> " ++ fnl () ++
- hov 0 (prlist pr_hints_db valid_dbs))
+ hov 0 (prlist (pr_hints_db env sigma) valid_dbs))
let pr_hint_ref ref = pr_hint_list_for_head ref
(* Print all hints associated to head id in any database *)
-let pr_hint_term sigma cl =
+let pr_hint_term env sigma cl =
try
let dbs = current_db () in
let valid_dbs =
@@ -1460,18 +1460,19 @@ let pr_hint_term sigma cl =
(str "No hint applicable for current goal")
else
(str "Applicable Hints :" ++ fnl () ++
- hov 0 (prlist pr_hints_db valid_dbs))
+ hov 0 (prlist (pr_hints_db env sigma) valid_dbs))
with Match_failure _ | Failure _ ->
(str "No hint applicable for current goal")
(* print all hints that apply to the concl of the current goal *)
let pr_applicable_hint () =
+ let env = Global.env () in
let pts = Proof_global.give_me_the_proof () in
- let glss = Proof.V82.subgoals pts in
- match glss.Evd.it with
+ let glss,_,_,_,sigma = Proof.proof pts in
+ match glss with
| [] -> CErrors.user_err Pp.(str "No focused goal.")
| g::_ ->
- pr_hint_term glss.Evd.sigma (Goal.V82.concl glss.Evd.sigma g)
+ pr_hint_term env sigma (Goal.V82.concl sigma g)
let pp_hint_mode = function
| ModeInput -> str"+"
@@ -1479,9 +1480,9 @@ let pp_hint_mode = function
| ModeOutput -> str"-"
(* displays the whole hint database db *)
-let pr_hint_db db =
+let pr_hint_db_env env sigma db =
let pr_mode = prvect_with_sep spc pp_hint_mode in
- let pr_modes l =
+ let pr_modes l =
if List.is_empty l then mt ()
else str" (modes " ++ prlist_with_sep pr_comma pr_mode l ++ str")"
in
@@ -1491,7 +1492,7 @@ let pr_hint_db db =
| None -> str "For any goal"
| Some head -> str "For " ++ pr_global head ++ pr_modes modes
in
- let hints = pr_hint_list (List.map (fun x -> (0, x)) hintlist) in
+ let hints = pr_hint_list env sigma (List.map (fun x -> (0, x)) hintlist) in
let hint_descr = hov 0 (goal_descr ++ str " -> " ++ hints) in
accu ++ hint_descr
in
@@ -1506,17 +1507,21 @@ let pr_hint_db db =
hov 2 (str"Cut: " ++ pp_hints_path (Hint_db.cut db)) ++ fnl () ++
content
-let pr_hint_db_by_name dbname =
+let pr_hint_db db =
+ let sigma, env = Pfedit.get_current_context () in
+ pr_hint_db_env env sigma db
+
+let pr_hint_db_by_name env sigma dbname =
try
- let db = searchtable_map dbname in pr_hint_db db
+ let db = searchtable_map dbname in pr_hint_db_env env sigma db
with Not_found ->
error_no_such_hint_database dbname
(* displays all the hints of all databases *)
-let pr_searchtable () =
+let pr_searchtable env sigma =
let fold name db accu =
accu ++ str "In the database " ++ str name ++ str ":" ++ fnl () ++
- pr_hint_db db ++ fnl ()
+ pr_hint_db_env env sigma db ++ fnl ()
in
Hintdbmap.fold fold !searchtable (mt ())
@@ -1534,10 +1539,13 @@ let warn_non_imported_hint =
strbrk "Hint used but not imported: " ++ hint ++ print_mp mp)
let warn h x =
- let hint = pr_hint h in
- let (mp, _, _) = KerName.repr h.uid in
- warn_non_imported_hint (hint,mp);
- Proofview.tclUNIT x
+ let open Proofview in
+ tclBIND tclENV (fun env ->
+ tclBIND tclEVARMAP (fun sigma ->
+ let hint = pr_hint env sigma h in
+ let (mp, _, _) = KerName.repr h.uid in
+ warn_non_imported_hint (hint,mp);
+ Proofview.tclUNIT x))
let run_hint tac k = match !warn_hint with
| `LAX -> k tac.obj
diff --git a/tactics/hints.mli b/tactics/hints.mli
index 22df29b80..cbf204981 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -260,14 +260,15 @@ val rewrite_db : hint_db_name
(** Printing hints *)
-val pr_searchtable : unit -> Pp.t
+val pr_searchtable : env -> evar_map -> Pp.t
val pr_applicable_hint : unit -> Pp.t
-val pr_hint_ref : global_reference -> Pp.t
-val pr_hint_db_by_name : hint_db_name -> Pp.t
+val pr_hint_ref : env -> evar_map -> global_reference -> Pp.t
+val pr_hint_db_by_name : env -> evar_map -> hint_db_name -> Pp.t
+val pr_hint_db_env : env -> evar_map -> Hint_db.t -> Pp.t
val pr_hint_db : Hint_db.t -> Pp.t
-val pr_hint : hint -> 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
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 8648dfb90..46b10bf33 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -282,10 +282,11 @@ let generalizeRewriteIntros as_mode tac depids id =
let error_too_many_names pats =
let loc = Loc.merge_opt (fst (List.hd pats)) (fst (List.last pats)) in
Proofview.tclENV >>= fun env ->
+ Proofview.tclEVARMAP >>= fun sigma ->
tclZEROMSG ?loc (
str "Unexpected " ++
str (String.plural (List.length pats) "introduction pattern") ++
- str ": " ++ pr_enum (Miscprint.pr_intro_pattern (fun c -> Printer.pr_constr (EConstr.Unsafe.to_constr (snd (c env Evd.empty))))) pats ++
+ str ": " ++ pr_enum (Miscprint.pr_intro_pattern (fun c -> Printer.pr_constr_env env sigma (EConstr.Unsafe.to_constr (snd (c env Evd.empty))))) pats ++
str ".")
let get_names (allow_conj,issimple) (loc, pat as x) = match pat with
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index cc9d98f6f..62f3866de 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -215,7 +215,7 @@ let inversion_scheme env sigma t sort dep_option inv_op =
invEnv ~init:Context.Named.empty
end in
let avoid = ref Id.Set.empty in
- let { sigma=sigma } = Proof.V82.subgoals pf in
+ let _,_,_,_,sigma = Proof.proof pf in
let sigma = Evd.nf_constraints sigma in
let rec fill_holes c =
match EConstr.kind sigma c with
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 15c25b346..e072bd95f 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -945,10 +945,14 @@ let reduction_clause redexp cl =
(None, bind_red_expr_occurrences occs nbcl redexp)) cl
let reduce redexp cl =
- let trace () =
+ let trace env sigma =
let open Printer in
- let pr = (pr_econstr, pr_leconstr, pr_evaluable_reference, pr_constr_pattern) in
- Pp.(hov 2 (Pputils.pr_red_expr pr str redexp))
+ let pr = (pr_econstr_env, pr_leconstr_env, pr_evaluable_reference, pr_constr_pattern_env) in
+ Pp.(hov 2 (Pputils.pr_red_expr_env env sigma pr str redexp))
+ in
+ let trace () =
+ let sigma, env = Pfedit.get_current_context () in
+ trace env sigma
in
Proofview.Trace.name_tactic trace begin
Proofview.Goal.enter begin fun gl ->
@@ -3128,11 +3132,11 @@ let expand_hyp id = Tacticals.New.tclTRY (unfold_body id) <*> clear [id]
let warn_unused_intro_pattern env sigma =
CWarnings.create ~name:"unused-intro-pattern" ~category:"tactics"
- (fun names ->
- strbrk"Unused introduction " ++ str (String.plural (List.length names) "pattern")
- ++ str": " ++ prlist_with_sep spc
- (Miscprint.pr_intro_pattern
- (fun c -> Printer.pr_econstr (snd (c env sigma)))) names)
+ (fun names ->
+ strbrk"Unused introduction " ++ str (String.plural (List.length names) "pattern") ++
+ str": " ++ prlist_with_sep spc
+ (Miscprint.pr_intro_pattern
+ (fun c -> Printer.pr_econstr_env env sigma (snd (c env sigma)))) names)
let check_unused_names env sigma names =
if not (List.is_empty names) then
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-08 09:26:11 +0000