aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/ppconstr.ml
diff options
context:
space:
mode:
Diffstat (limited to 'parsing/ppconstr.ml')
-rw-r--r--parsing/ppconstr.ml12
1 files changed, 6 insertions, 6 deletions
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index f5fe151ed..e16641a83 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -666,15 +666,15 @@ let rec strip_context n iscast t =
type term_pr = {
pr_constr_expr : constr_expr -> std_ppcmds;
pr_lconstr_expr : constr_expr -> std_ppcmds;
- pr_pattern_expr : Tacexpr.pattern_expr -> std_ppcmds;
- pr_lpattern_expr : Tacexpr.pattern_expr -> std_ppcmds
+ pr_constr_pattern_expr : constr_pattern_expr -> std_ppcmds;
+ pr_lconstr_pattern_expr : constr_pattern_expr -> std_ppcmds
}
let default_term_pr = {
pr_constr_expr = pr lsimple;
pr_lconstr_expr = pr ltop;
- pr_pattern_expr = pr lsimple;
- pr_lpattern_expr = pr ltop
+ pr_constr_pattern_expr = pr lsimple;
+ pr_lconstr_pattern_expr = pr ltop
}
let term_pr = ref default_term_pr
@@ -683,8 +683,8 @@ let set_term_pr = (:=) term_pr
let pr_constr_expr c = !term_pr.pr_constr_expr c
let pr_lconstr_expr c = !term_pr.pr_lconstr_expr c
-let pr_pattern_expr c = !term_pr.pr_pattern_expr c
-let pr_lpattern_expr c = !term_pr.pr_lpattern_expr c
+let pr_constr_pattern_expr c = !term_pr.pr_constr_pattern_expr c
+let pr_lconstr_pattern_expr c = !term_pr.pr_lconstr_pattern_expr c
let pr_cases_pattern_expr = pr_patt ltop