aboutsummaryrefslogtreecommitdiff
path: root/parsing/ppconstr.mli
diff options
context:
space:
mode:
Diffstat (limited to 'parsing/ppconstr.mli')
-rw-r--r--parsing/ppconstr.mli8
1 files changed, 4 insertions, 4 deletions
diff --git a/parsing/ppconstr.mli b/parsing/ppconstr.mli
index b9bf933ebd..d7fdd1ed95 100644
--- a/parsing/ppconstr.mli
+++ b/parsing/ppconstr.mli
@@ -66,8 +66,8 @@ val pr_may_eval :
val pr_rawsort : rawsort -> std_ppcmds
val pr_binders : local_binder list -> std_ppcmds
-val pr_pattern_expr : Tacexpr.pattern_expr -> std_ppcmds
-val pr_lpattern_expr : Tacexpr.pattern_expr -> std_ppcmds
+val pr_constr_pattern_expr : constr_pattern_expr -> std_ppcmds
+val pr_lconstr_pattern_expr : constr_pattern_expr -> std_ppcmds
val pr_constr_expr : constr_expr -> std_ppcmds
val pr_lconstr_expr : constr_expr -> std_ppcmds
val pr_cases_pattern_expr : cases_pattern_expr -> std_ppcmds
@@ -75,8 +75,8 @@ val pr_cases_pattern_expr : cases_pattern_expr -> std_ppcmds
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
}
val set_term_pr : term_pr -> unit