aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--dev/top_printers.ml3
-rw-r--r--printing/pptactic.ml76
-rw-r--r--printing/pptacticsig.mli45
-rw-r--r--printing/ppvernac.ml8
-rw-r--r--tactics/tacinterp.ml4
5 files changed, 62 insertions, 74 deletions
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index b3b1ae0e91..0e90026122 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -468,9 +468,8 @@ let pp_generic_argument arg =
let prgenarginfo arg =
let tpe = pr_argument_type (genarg_tag arg) in
- let pr_gtac _ x = Pptactic.pr_glob_tactic (Global.env()) x in
try
- let data = Pptactic.pr_top_generic pr_constr pr_lconstr pr_gtac pr_constr_pattern arg in
+ let data = Pptactic.pr_top_generic (Global.env ()) arg in
str "<genarg:" ++ tpe ++ str " := [ " ++ data ++ str " ] >"
with _any ->
str "<genarg:" ++ tpe ++ str ">"
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index dfb8837eca..4d14cae7a7 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -265,12 +265,12 @@ module Make
let with_evars ev s = if ev then "e" ^ s else s
- let rec pr_raw_generic prc prlc prtac prpat prref (x:Genarg.rlevel Genarg.generic_argument) =
+ let rec pr_raw_generic_rec prc prlc prtac prpat prref (x:Genarg.rlevel Genarg.generic_argument) =
match Genarg.genarg_tag x with
| IntOrVarArgType -> pr_or_var int (out_gen (rawwit wit_int_or_var) x)
| IdentArgType -> pr_id (out_gen (rawwit wit_ident) x)
| VarArgType -> pr_located pr_id (out_gen (rawwit wit_var) x)
- | GenArgType -> pr_raw_generic prc prlc prtac prpat prref (out_gen (rawwit wit_genarg) x)
+ | GenArgType -> pr_raw_generic_rec prc prlc prtac prpat prref (out_gen (rawwit wit_genarg) x)
| ConstrArgType -> prc (out_gen (rawwit wit_constr) x)
| ConstrMayEvalArgType ->
pr_may_eval prc prlc (pr_or_by_notation prref) prpat
@@ -278,14 +278,14 @@ module Make
| OpenConstrArgType -> prc (snd (out_gen (rawwit wit_open_constr) x))
| ListArgType _ ->
let list_unpacker wit l =
- let map x = pr_raw_generic prc prlc prtac prpat prref (in_gen (rawwit wit) x) in
+ let map x = pr_raw_generic_rec prc prlc prtac prpat prref (in_gen (rawwit wit) x) in
pr_sequence map (raw l)
in
hov 0 (list_unpack { list_unpacker } x)
| OptArgType _ ->
let opt_unpacker wit o = match raw o with
| None -> mt ()
- | Some x -> pr_raw_generic prc prlc prtac prpat prref (in_gen (rawwit wit) x)
+ | Some x -> pr_raw_generic_rec prc prlc prtac prpat prref (in_gen (rawwit wit) x)
in
hov 0 (opt_unpack { opt_unpacker } x)
| PairArgType _ ->
@@ -293,7 +293,7 @@ module Make
let p, q = raw o in
let p = in_gen (rawwit wit1) p in
let q = in_gen (rawwit wit2) q in
- pr_sequence (pr_raw_generic prc prlc prtac prpat prref) [p; q]
+ pr_sequence (pr_raw_generic_rec prc prlc prtac prpat prref) [p; q]
in
hov 0 (pair_unpack { pair_unpacker } x)
| ExtraArgType s ->
@@ -301,12 +301,12 @@ module Make
with Not_found -> Genprint.generic_raw_print x
- let rec pr_glb_generic prc prlc prtac prpat x =
+ let rec pr_glb_generic_rec prc prlc prtac prpat x =
match Genarg.genarg_tag x with
| IntOrVarArgType -> pr_or_var int (out_gen (glbwit wit_int_or_var) x)
| IdentArgType -> pr_id (out_gen (glbwit wit_ident) x)
| VarArgType -> pr_located pr_id (out_gen (glbwit wit_var) x)
- | GenArgType -> pr_glb_generic prc prlc prtac prpat (out_gen (glbwit wit_genarg) x)
+ | GenArgType -> pr_glb_generic_rec prc prlc prtac prpat (out_gen (glbwit wit_genarg) x)
| ConstrArgType -> prc (out_gen (glbwit wit_constr) x)
| ConstrMayEvalArgType ->
pr_may_eval prc prlc
@@ -315,14 +315,14 @@ module Make
| OpenConstrArgType -> prc (snd (out_gen (glbwit wit_open_constr) x))
| ListArgType _ ->
let list_unpacker wit l =
- let map x = pr_glb_generic prc prlc prtac prpat (in_gen (glbwit wit) x) in
+ let map x = pr_glb_generic_rec prc prlc prtac prpat (in_gen (glbwit wit) x) in
pr_sequence map (glb l)
in
hov 0 (list_unpack { list_unpacker } x)
| OptArgType _ ->
let opt_unpacker wit o = match glb o with
| None -> mt ()
- | Some x -> pr_glb_generic prc prlc prtac prpat (in_gen (glbwit wit) x)
+ | Some x -> pr_glb_generic_rec prc prlc prtac prpat (in_gen (glbwit wit) x)
in
hov 0 (opt_unpack { opt_unpacker } x)
| PairArgType _ ->
@@ -330,32 +330,32 @@ module Make
let p, q = glb o in
let p = in_gen (glbwit wit1) p in
let q = in_gen (glbwit wit2) q in
- pr_sequence (pr_glb_generic prc prlc prtac prpat) [p; q]
+ pr_sequence (pr_glb_generic_rec prc prlc prtac prpat) [p; q]
in
hov 0 (pair_unpack { pair_unpacker } x)
| ExtraArgType s ->
try pi2 (String.Map.find s !genarg_pprule) prc prlc prtac x
with Not_found -> Genprint.generic_glb_print x
- let rec pr_top_generic prc prlc prtac prpat x =
+ let rec pr_top_generic_rec prc prlc prtac prpat x =
match Genarg.genarg_tag x with
| IntOrVarArgType -> pr_or_var int (out_gen (topwit wit_int_or_var) x)
| IdentArgType -> pr_id (out_gen (topwit wit_ident) x)
| VarArgType -> pr_id (out_gen (topwit wit_var) x)
- | GenArgType -> pr_top_generic prc prlc prtac prpat (out_gen (topwit wit_genarg) x)
+ | GenArgType -> pr_top_generic_rec prc prlc prtac prpat (out_gen (topwit wit_genarg) x)
| ConstrArgType -> prc (out_gen (topwit wit_constr) x)
| ConstrMayEvalArgType -> prc (out_gen (topwit wit_constr_may_eval) x)
| OpenConstrArgType -> prc (snd (out_gen (topwit wit_open_constr) x))
| ListArgType _ ->
let list_unpacker wit l =
- let map x = pr_top_generic prc prlc prtac prpat (in_gen (topwit wit) x) in
+ let map x = pr_top_generic_rec prc prlc prtac prpat (in_gen (topwit wit) x) in
pr_sequence map (top l)
in
hov 0 (list_unpack { list_unpacker } x)
| OptArgType _ ->
let opt_unpacker wit o = match top o with
| None -> mt ()
- | Some x -> pr_top_generic prc prlc prtac prpat (in_gen (topwit wit) x)
+ | Some x -> pr_top_generic_rec prc prlc prtac prpat (in_gen (topwit wit) x)
in
hov 0 (opt_unpack { opt_unpacker } x)
| PairArgType _ ->
@@ -363,7 +363,7 @@ module Make
let p, q = top o in
let p = in_gen (topwit wit1) p in
let q = in_gen (topwit wit2) q in
- pr_sequence (pr_top_generic prc prlc prtac prpat) [p; q]
+ pr_sequence (pr_top_generic_rec prc prlc prtac prpat) [p; q]
in
hov 0 (pair_unpack { pair_unpacker } x)
| ExtraArgType s ->
@@ -415,19 +415,19 @@ module Make
with Not_found ->
KerName.print key ++ spc() ++ pr_sequence pr_gen l ++ str" (* Generic printer *)"
- let pr_raw_extend prc prlc prtac prpat =
- pr_extend_gen (pr_raw_generic prc prlc prtac prpat pr_reference)
- let pr_glob_extend prc prlc prtac prpat =
- pr_extend_gen (pr_glb_generic prc prlc prtac prpat)
- let pr_extend prc prlc prtac prpat =
- pr_extend_gen (pr_top_generic prc prlc prtac prpat)
+ let pr_raw_extend_rec prc prlc prtac prpat =
+ pr_extend_gen (pr_raw_generic_rec prc prlc prtac prpat pr_reference)
+ let pr_glob_extend_rec prc prlc prtac prpat =
+ pr_extend_gen (pr_glb_generic_rec prc prlc prtac prpat)
+ let pr_extend_rec prc prlc prtac prpat =
+ pr_extend_gen (pr_top_generic_rec prc prlc prtac prpat)
let pr_raw_alias prc prlc prtac prpat =
- pr_alias_gen (pr_raw_generic prc prlc prtac prpat pr_reference)
+ pr_alias_gen (pr_raw_generic_rec prc prlc prtac prpat pr_reference)
let pr_glob_alias prc prlc prtac prpat =
- pr_alias_gen (pr_glb_generic prc prlc prtac prpat)
+ pr_alias_gen (pr_glb_generic_rec prc prlc prtac prpat)
let pr_alias prc prlc prtac prpat =
- pr_alias_gen (pr_top_generic prc prlc prtac prpat)
+ pr_alias_gen (pr_top_generic_rec prc prlc prtac prpat)
(**********************************************************************)
(* The tactic printer *)
@@ -1282,7 +1282,7 @@ module Make
pr_reference = pr_reference;
pr_name = pr_lident;
pr_generic = Genprint.generic_raw_print;
- pr_extend = pr_raw_extend pr_constr_expr pr_lconstr_expr pr_raw_tactic_level pr_constr_pattern_expr;
+ pr_extend = pr_raw_extend_rec pr_constr_expr pr_lconstr_expr pr_raw_tactic_level pr_constr_pattern_expr;
pr_alias = pr_raw_alias pr_constr_expr pr_lconstr_expr pr_raw_tactic_level pr_constr_pattern_expr;
} in
make_pr_tac
@@ -1313,7 +1313,7 @@ module Make
pr_reference = pr_ltac_or_var (pr_located pr_ltac_constant);
pr_name = pr_lident;
pr_generic = Genprint.generic_glb_print;
- pr_extend = pr_glob_extend
+ pr_extend = pr_glob_extend_rec
(pr_and_constr_expr (pr_glob_constr_env env)) (pr_and_constr_expr (pr_lglob_constr_env env))
prtac (pr_pat_and_constr_expr (pr_glob_constr_env env));
pr_alias = pr_glob_alias
@@ -1355,7 +1355,7 @@ module Make
pr_reference = pr_located pr_ltac_constant;
pr_name = pr_id;
pr_generic = Genprint.generic_top_print;
- pr_extend = pr_extend
+ pr_extend = pr_extend_rec
(pr_constr_env env Evd.empty) (pr_lconstr_env env Evd.empty)
(pr_glob_tactic_level env) pr_constr_pattern;
pr_alias = pr_alias
@@ -1370,6 +1370,28 @@ module Make
in
prtac n t
+ let pr_raw_generic env = pr_raw_generic_rec
+ pr_constr_expr pr_lconstr_expr pr_raw_tactic_level pr_constr_pattern_expr pr_reference
+
+ let pr_glb_generic env = pr_glb_generic_rec
+ (pr_and_constr_expr (pr_glob_constr_env env)) (pr_and_constr_expr (pr_lglob_constr_env env))
+ (pr_glob_tactic_level env) (pr_pat_and_constr_expr (pr_glob_constr_env env))
+
+ let pr_top_generic env = pr_top_generic_rec
+ (pr_constr_env env Evd.empty) (pr_lconstr_env env Evd.empty)
+ (pr_glob_tactic_level env) pr_constr_pattern
+
+ let pr_raw_extend env = pr_raw_extend_rec
+ pr_constr_expr pr_lconstr_expr pr_raw_tactic_level pr_constr_pattern_expr
+
+ let pr_glob_extend env = pr_glob_extend_rec
+ (pr_and_constr_expr (pr_glob_constr_env env)) (pr_and_constr_expr (pr_lglob_constr_env env))
+ (pr_glob_tactic_level env) (pr_pat_and_constr_expr (pr_glob_constr_env env))
+
+ let pr_extend env = pr_extend_rec
+ (pr_constr_env env Evd.empty) (pr_lconstr_env env Evd.empty)
+ (pr_glob_tactic_level env) pr_constr_pattern
+
let pr_tactic env = pr_tactic_level env ltop
end
diff --git a/printing/pptacticsig.mli b/printing/pptacticsig.mli
index 1631bda377..1c17d04928 100644
--- a/printing/pptacticsig.mli
+++ b/printing/pptacticsig.mli
@@ -32,45 +32,20 @@ module type Pp = sig
val pr_clauses : bool option ->
('a -> Pp.std_ppcmds) -> 'a Locus.clause_expr -> Pp.std_ppcmds
- val pr_raw_generic :
- (constr_expr -> std_ppcmds) ->
- (constr_expr -> std_ppcmds) ->
- (tolerability -> raw_tactic_expr -> std_ppcmds) ->
- (constr_expr -> std_ppcmds) ->
- (Libnames.reference -> std_ppcmds) -> rlevel generic_argument ->
- std_ppcmds
-
- val pr_glb_generic :
- (glob_constr_and_expr -> Pp.std_ppcmds) ->
- (glob_constr_and_expr -> Pp.std_ppcmds) ->
- (tolerability -> glob_tactic_expr -> std_ppcmds) ->
- (glob_constr_pattern_and_expr -> std_ppcmds) ->
- glevel generic_argument -> std_ppcmds
-
- val pr_top_generic :
- (Term.constr -> std_ppcmds) ->
- (Term.constr -> std_ppcmds) ->
- (tolerability -> glob_tactic_expr -> std_ppcmds) ->
- (Pattern.constr_pattern -> std_ppcmds) ->
- tlevel generic_argument ->
- std_ppcmds
-
- val pr_raw_extend:
- (constr_expr -> std_ppcmds) -> (constr_expr -> std_ppcmds) ->
- (tolerability -> raw_tactic_expr -> std_ppcmds) ->
- (constr_expr -> std_ppcmds) -> int ->
+
+ val pr_raw_generic : env -> rlevel generic_argument -> std_ppcmds
+
+ val pr_glb_generic : env -> glevel generic_argument -> std_ppcmds
+
+ val pr_top_generic : env -> tlevel generic_argument -> std_ppcmds
+
+ val pr_raw_extend: env -> int ->
ml_tactic_entry -> raw_generic_argument list -> std_ppcmds
- val pr_glob_extend:
- (glob_constr_and_expr -> std_ppcmds) -> (glob_constr_and_expr -> std_ppcmds) ->
- (tolerability -> glob_tactic_expr -> std_ppcmds) ->
- (glob_constr_pattern_and_expr -> std_ppcmds) -> int ->
+ val pr_glob_extend: env -> int ->
ml_tactic_entry -> glob_generic_argument list -> std_ppcmds
- val pr_extend :
- (Term.constr -> std_ppcmds) -> (Term.constr -> std_ppcmds) ->
- (tolerability -> glob_tactic_expr -> std_ppcmds) ->
- (constr_pattern -> std_ppcmds) -> int ->
+ val pr_extend : env -> int ->
ml_tactic_entry -> typed_generic_argument list -> std_ppcmds
val pr_ltac_constant : Nametab.ltac_constant -> std_ppcmds
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 72b9cafe3f..d79fb45618 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -79,13 +79,7 @@ module Make
| VernacEndSubproof -> str""
| _ -> str"."
- let pr_gen t =
- pr_raw_generic
- pr_constr_expr
- pr_lconstr_expr
- pr_raw_tactic_level
- pr_constr_expr
- pr_reference t
+ let pr_gen t = pr_raw_generic (Global.env ()) t
let sep = fun _ -> spc()
let sep_v2 = fun _ -> str"," ++ spc()
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 6ac16bd76a..3295b932b9 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -60,9 +60,7 @@ let push_appl appl args =
| UnnamedAppl -> UnnamedAppl
| GlbAppl l -> GlbAppl (List.map (fun (h,vs) -> (h,vs@args)) l)
let pr_generic arg =
- let pr_gtac _ x = Pptactic.pr_glob_tactic (Global.env()) x in
- try
- Pptactic.pr_top_generic pr_constr pr_lconstr pr_gtac pr_constr_pattern arg
+ try Pptactic.pr_top_generic (Global.env ()) arg
with e when Errors.noncritical e -> str"<generic>"
let pr_appl h vs =
Pptactic.pr_ltac_constant h ++ spc () ++
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 16:25:14 +0000