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 7cc193a8d..f8264e5af 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -1451,7 +1451,7 @@ let () = (pr_clauses (Some true) (fun id -> pr_lident (Loc.ghost,id))) ; Genprint.register_print0 Constrarg.wit_sort - pr_glob_sort pr_glob_sort pr_sort; + pr_glob_sort pr_glob_sort (pr_sort Evd.empty); Genprint.register_print0 Constrarg.wit_uconstr Ppconstr.pr_constr_expr |