diff options
author | 2016-04-27 22:13:03 +0200 | |
---|---|---|
committer | 2016-04-27 22:13:03 +0200 | |
commit | 172708b434ead6c3f824cf51e60c3141597e1e2b (patch) | |
tree | faf3943ea63e9955f165cc5d5c85079cd0da3b88 /printing/pptactic.ml | |
parent | bfd23b1ec7e6c29c1740ec3c917851cbdb6ec18e (diff) |
Revert "Fixing printing of induction/destruct as."
This reverts commit 691dc7d88c6810333eecef7c2f0b8d8617d19ab1.
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 3ebb37084..06bf07741 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -863,7 +863,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_non_empty_arg (pr_with_induction_names pr.pr_dconstr) ids ++ + pr_with_induction_names pr.pr_dconstr ids ++ pr_opt (pr_clauses None pr.pr_name) cl) l ++ pr_opt pr_eliminator el ) |