aboutsummaryrefslogtreecommitdiff
path: root/plugins/ltac/pptactic.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ltac/pptactic.ml')
-rw-r--r--plugins/ltac/pptactic.ml98
1 files changed, 26 insertions, 72 deletions
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index 75ab1c5ee6..8300a55e3d 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -6,6 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
+open API
open Pp
open Names
open Namegen
@@ -161,28 +162,6 @@ type 'a extra_genarg_printer =
| AnonHyp n -> int n
| NamedHyp id -> pr_id id
- let pr_binding prc = function
- | loc, (NamedHyp id, c) -> hov 1 (pr_id id ++ str " := " ++ cut () ++ prc c)
- | loc, (AnonHyp n, c) -> hov 1 (int n ++ str " := " ++ cut () ++ prc c)
-
- let pr_bindings prc prlc = function
- | ImplicitBindings l ->
- brk (1,1) ++ keyword "with" ++ brk (1,1) ++
- hv 0 (prlist_with_sep spc prc l)
- | ExplicitBindings l ->
- brk (1,1) ++ keyword "with" ++ brk (1,1) ++
- hv 0 (prlist_with_sep spc (fun b -> str"(" ++ pr_binding prlc b ++ str")") l)
- | NoBindings -> mt ()
-
- let pr_bindings_no_with prc prlc = function
- | ImplicitBindings l ->
- brk (0,1) ++
- prlist_with_sep spc prc l
- | ExplicitBindings l ->
- brk (0,1) ++
- prlist_with_sep spc (fun b -> str"(" ++ pr_binding prlc b ++ str")") l
- | NoBindings -> mt ()
-
let pr_clear_flag clear_flag pp x =
match clear_flag with
| Some false -> surround (pp x)
@@ -190,7 +169,7 @@ type 'a extra_genarg_printer =
| None -> pp x
let pr_with_bindings prc prlc (c,bl) =
- prc c ++ pr_bindings prc prlc bl
+ prc c ++ Miscprint.pr_bindings prc prlc bl
let pr_with_bindings_arg prc prlc (clear_flag,c) =
pr_clear_flag clear_flag (pr_with_bindings prc prlc) c
@@ -348,7 +327,7 @@ type 'a extra_genarg_printer =
let bll = List.map (fun (x, _, y) -> x, y) bll in
if nb >= n then (List.rev (bll@acc)), a
else strip_ty (bll@acc) (n-nb) a
- | _ -> error "Cannot translate fix tactic: not enough products" in
+ | _ -> user_err Pp.(str "Cannot translate fix tactic: not enough products") in
strip_ty [] n ty
let pr_ltac_or_var pr = function
@@ -356,41 +335,17 @@ type 'a extra_genarg_printer =
| ArgVar (loc,id) -> pr_with_comments ?loc (pr_id id)
let pr_ltac_constant kn =
- if !Flags.in_debugger then pr_kn kn
+ if !Flags.in_debugger then KerName.print kn
else try
pr_qualid (Nametab.shortest_qualid_of_tactic kn)
with Not_found -> (* local tactic not accessible anymore *)
- str "<" ++ pr_kn kn ++ str ">"
+ str "<" ++ KerName.print kn ++ str ">"
let pr_evaluable_reference_env env = function
| EvalVarRef id -> pr_id id
| EvalConstRef sp ->
Nametab.pr_global_env (Termops.vars_of_env env) (Globnames.ConstRef sp)
- let pr_esubst prc l =
- let pr_qhyp = function
- (_,(AnonHyp n,c)) -> str "(" ++ int n ++ str" := " ++ prc c ++ str ")"
- | (_,(NamedHyp id,c)) ->
- str "(" ++ pr_id id ++ str" := " ++ prc c ++ str ")"
- in
- prlist_with_sep spc pr_qhyp l
-
- let pr_bindings_gen for_ex prc prlc = function
- | ImplicitBindings l ->
- spc () ++
- hv 2 ((if for_ex then mt() else keyword "with" ++ spc ()) ++
- prlist_with_sep spc prc l)
- | ExplicitBindings l ->
- spc () ++
- hv 2 ((if for_ex then mt() else keyword "with" ++ spc ()) ++
- pr_esubst prlc l)
- | NoBindings -> mt ()
-
- let pr_bindings prc prlc = pr_bindings_gen false prc prlc
-
- let pr_with_bindings prc prlc (c,bl) =
- hov 1 (prc c ++ pr_bindings prc prlc bl)
-
let pr_as_disjunctive_ipat prc ipatl =
keyword "as" ++ spc () ++
pr_or_var (fun (loc,p) -> Miscprint.pr_or_and_intro_pattern prc p) ipatl
@@ -527,7 +482,7 @@ type 'a extra_genarg_printer =
| SelectNth i -> int i ++ str ":"
| SelectList l -> str "[" ++ prlist_with_sep (fun () -> str ", ") pr_range_selector l ++
str "]" ++ str ":"
- | SelectId id -> str "[" ++ Nameops.pr_id id ++ str "]" ++ str ":"
+ | SelectId id -> str "[" ++ Id.print id ++ str "]" ++ str ":"
| SelectAll -> str "all" ++ str ":"
let pr_lazy = function
@@ -571,7 +526,7 @@ type 'a extra_genarg_printer =
str "=>" ++ brk (1,4) ++ pr t))
| All t -> str "_" ++ spc () ++ str "=>" ++ brk (1,4) ++ pr t
- let pr_funvar n = spc () ++ pr_name n
+ let pr_funvar n = spc () ++ Name.print n
let pr_let_clause k pr (id,(bl,t)) =
hov 0 (keyword k ++ spc () ++ pr_lident id ++ prlist pr_funvar bl ++
@@ -582,7 +537,7 @@ type 'a extra_genarg_printer =
hv 0
(pr_let_clause (if recflag then "let rec" else "let") pr hd ++
prlist (fun t -> spc () ++ pr_let_clause "with" pr t) tl)
- | [] -> anomaly (Pp.str "LetIn must declare at least one binding")
+ | [] -> anomaly (Pp.str "LetIn must declare at least one binding.")
let pr_seq_body pr tl =
hv 0 (str "[ " ++
@@ -768,15 +723,15 @@ type 'a extra_genarg_printer =
primitive "cofix" ++ spc () ++ pr_id id ++ spc()
++ keyword "with" ++ spc () ++ prlist_with_sep spc pr_cofix_tac l
)
- | TacAssert (b,Some tac,ipat,c) ->
+ | TacAssert (ev,b,Some tac,ipat,c) ->
hov 1 (
- primitive (if b then "assert" else "enough") ++
+ primitive (if b then if ev then "eassert" else "assert" else if ev then "eenough" else "enough") ++
pr_assumption pr.pr_constr pr.pr_dconstr pr.pr_lconstr ipat c ++
pr_non_empty_arg (pr_by_tactic (pr.pr_tactic (ltactical,E))) tac
)
- | TacAssert (_,None,ipat,c) ->
+ | TacAssert (ev,_,None,ipat,c) ->
hov 1 (
- primitive "pose proof"
+ primitive (if ev then "epose proof" else "pose proof")
++ pr_assertion pr.pr_constr pr.pr_dconstr pr.pr_lconstr ipat c
)
| TacGeneralize l ->
@@ -786,11 +741,11 @@ type 'a extra_genarg_printer =
pr_with_occurrences pr.pr_constr cl ++ pr_as_name na)
l
)
- | TacLetTac (na,c,cl,true,_) when Locusops.is_nowhere cl ->
- hov 1 (primitive "pose" ++ pr_pose pr.pr_constr pr.pr_lconstr na c)
- | TacLetTac (na,c,cl,b,e) ->
+ | TacLetTac (ev,na,c,cl,true,_) when Locusops.is_nowhere cl ->
+ hov 1 (primitive (if ev then "epose" else "pose") ++ pr_pose pr.pr_constr pr.pr_lconstr na c)
+ | TacLetTac (ev,na,c,cl,b,e) ->
hov 1 (
- (if b then primitive "set" else primitive "remember") ++
+ primitive (if b then if ev then "eset" else "set" else if ev then "eremember" else "remember") ++
(if b then pr_pose pr.pr_constr pr.pr_lconstr na c
else pr_pose_as_style pr.pr_constr na c) ++
pr_opt (fun p -> pr_eqn_ipat p ++ spc ()) e ++
@@ -1089,7 +1044,7 @@ type 'a extra_genarg_printer =
match ty.CAst.v with
Glob_term.GProd(na,Explicit,a,b) ->
strip_ty (([Loc.tag na],(a,None))::acc) (n-1) b
- | _ -> error "Cannot translate fix tactic: not enough products" in
+ | _ -> user_err Pp.(str "Cannot translate fix tactic: not enough products") in
strip_ty [] n ty
let raw_printers =
@@ -1160,7 +1115,7 @@ type 'a extra_genarg_printer =
match Term.kind_of_term ty with
Term.Prod(na,a,b) ->
strip_ty (([Loc.tag na],EConstr.of_constr a)::acc) (n-1) b
- | _ -> error "Cannot translate fix tactic: not enough products" in
+ | _ -> user_err Pp.(str "Cannot translate fix tactic: not enough products") in
strip_ty [] n ty
let pr_atomic_tactic_level env sigma n t =
@@ -1210,7 +1165,7 @@ let declare_extra_genarg_pprule wit
(h : 'c extra_genarg_printer) =
begin match wit with
| ExtraArg s -> ()
- | _ -> error "Can declare a pretty-printing rule only for extra argument types."
+ | _ -> user_err Pp.(str "Can declare a pretty-printing rule only for extra argument types.")
end;
let f x = f pr_constr_expr pr_lconstr_expr pr_raw_tactic_level x in
let g x =
@@ -1225,11 +1180,10 @@ let declare_extra_genarg_pprule wit
(** Registering *)
-let run_delayed c =
- Sigma.run Evd.empty { Sigma.run = fun sigma -> c.delayed (Global.env ()) sigma }
+let run_delayed c = c (Global.env ()) Evd.empty
let run_delayed_destruction_arg = function (* HH: Using Evd.empty looks suspicious *)
- | clear_flag,ElimOnConstr g -> clear_flag,ElimOnConstr (fst (run_delayed g))
+ | clear_flag,ElimOnConstr g -> clear_flag,ElimOnConstr (snd (run_delayed g))
| clear_flag,ElimOnAnonHyp n as x -> x
| clear_flag,ElimOnIdent id as x -> x
@@ -1249,7 +1203,7 @@ let () =
wit_intro_pattern
(Miscprint.pr_intro_pattern pr_constr_expr)
(Miscprint.pr_intro_pattern (fun (c,_) -> pr_glob_constr c))
- (Miscprint.pr_intro_pattern (fun c -> pr_econstr (fst (run_delayed c))));
+ (Miscprint.pr_intro_pattern (fun c -> pr_econstr (snd (run_delayed c))));
Genprint.register_print0
wit_clause_dft_concl
(pr_clauses (Some true) pr_lident)
@@ -1280,13 +1234,13 @@ let () =
(pr_red_expr (pr_econstr, pr_leconstr, pr_evaluable_reference, pr_constr_pattern));
Genprint.register_print0 wit_quant_hyp pr_quantified_hypothesis pr_quantified_hypothesis pr_quantified_hypothesis;
Genprint.register_print0 wit_bindings
- (pr_bindings_no_with pr_constr_expr pr_lconstr_expr)
- (pr_bindings_no_with (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr))
- (fun it -> pr_bindings_no_with pr_econstr pr_leconstr (fst (run_delayed it)));
+ (Miscprint.pr_bindings_no_with pr_constr_expr pr_lconstr_expr)
+ (Miscprint.pr_bindings_no_with (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr))
+ (fun it -> Miscprint.pr_bindings_no_with pr_econstr pr_leconstr (snd (run_delayed it)));
Genprint.register_print0 wit_constr_with_bindings
(pr_with_bindings pr_constr_expr pr_lconstr_expr)
(pr_with_bindings (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr))
- (fun it -> pr_with_bindings pr_econstr pr_leconstr (fst (run_delayed it)));
+ (fun it -> pr_with_bindings pr_econstr pr_leconstr (snd (run_delayed it)));
Genprint.register_print0 Tacarg.wit_destruction_arg
(pr_destruction_arg pr_constr_expr pr_lconstr_expr)
(pr_destruction_arg (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr))
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 01:09:03 +0000