diff options
| author | Hugo Herbelin | 2016-04-27 22:13:03 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2016-04-27 22:13:03 +0200 |
| commit | 1e6cc18d36d57ca221d5807d106cf1ee229deeb4 (patch) | |
| tree | 1850f494291d93abee0722a1c9ad81aaa7c69947 | |
| parent | 1fe4593d355fcf305e36ebf4abf7e290ec37fab1 (diff) | |
Revert "Fixing printing of inversion as."
This reverts commit 6da8866a4fd79029b22bd1bf7cde6725a9ea259c.
| -rw-r--r-- | printing/pptactic.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/printing/pptactic.ml b/printing/pptactic.ml index 6f891c5f80..0afe9ae3bf 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -563,7 +563,7 @@ module Make | ElimOnIdent (loc,id) -> pr_with_comments loc (pr_id id) | ElimOnAnonHyp n -> int n - let pr_inversion_kind = function + let pr_induction_kind = function | SimpleInversion -> primitive "simple inversion" | FullInversion -> primitive "inversion" | FullInversionClear -> primitive "inversion_clear" @@ -918,16 +918,16 @@ module Make ) | TacInversion (DepInversion (k,c,ids),hyp) -> hov 1 ( - primitive "dependent " ++ pr_inversion_kind k ++ spc () + primitive "dependent " ++ pr_induction_kind k ++ spc () ++ pr_quantified_hypothesis hyp ++ pr_with_inversion_names pr.pr_dconstr ids ++ pr_with_constr pr.pr_constr c ) | TacInversion (NonDepInversion (k,cl,ids),hyp) -> hov 1 ( - pr_inversion_kind k ++ spc () + pr_induction_kind k ++ spc () ++ pr_quantified_hypothesis hyp - ++ pr_non_empty_arg (pr_with_inversion_names pr.pr_dconstr) ids + ++ pr_with_inversion_names pr.pr_dconstr ids ++ pr_non_empty_arg (pr_simple_hyp_clause pr.pr_name) cl ) | TacInversion (InversionUsing (c,cl),hyp) -> |