diff options
Diffstat (limited to 'printing/pptactic.ml')
| -rw-r--r-- | printing/pptactic.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/printing/pptactic.ml b/printing/pptactic.ml index 631cb4c577..7949bafcbb 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -1188,7 +1188,7 @@ module Make let pr_and_constr_expr pr (c,_) = pr c - let pr_pat_and_constr_expr pr ((c,_),_) = pr c + let pr_pat_and_constr_expr pr (_,(c,_),_) = pr c let pr_glob_tactic_level env n t = let glob_printers = |