diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-04-13 16:12:04 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-06-16 17:30:18 +0200 |
| commit | 0fc54db5d436d7e140c0363240a14268f6fd2c47 (patch) | |
| tree | 09a9273e1c7f765bc254992a1e51926c17fd02fc /printing | |
| parent | b2991bf6eec4ae7706f3dd33941af909f36f1773 (diff) | |
Fixing printing of induction/destruct as.
Diffstat (limited to 'printing')
| -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 3779a9412..4b4f04379 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -913,7 +913,7 @@ module Make ++ spc () ++ prlist_with_sep pr_comma (fun ((clear_flag,h),ids,cl) -> pr_clear_flag clear_flag (pr_induction_arg pr.pr_dconstr pr.pr_dconstr) h ++ - pr_with_induction_names pr.pr_dconstr ids ++ + pr_non_empty_arg (pr_with_induction_names pr.pr_dconstr) ids ++ pr_opt (pr_clauses None pr.pr_name) cl) l ++ pr_opt pr_eliminator el ) |