diff options
| author | Hugo Herbelin | 2016-04-16 16:45:44 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2016-04-27 21:55:46 +0200 |
| commit | 6da8866a4fd79029b22bd1bf7cde6725a9ea259c (patch) | |
| tree | cfa6eed557922f2f2434c4ab1d2e738d2a2da072 | |
| parent | 9b1b5de7a70c54ba3d60560d3d097f3eee2ca907 (diff) | |
Fixing printing of inversion as.
| -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 0afe9ae3bf..6f891c5f80 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_induction_kind = function + let pr_inversion_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_induction_kind k ++ spc () + primitive "dependent " ++ pr_inversion_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_induction_kind k ++ spc () + pr_inversion_kind k ++ spc () ++ pr_quantified_hypothesis hyp - ++ pr_with_inversion_names pr.pr_dconstr ids + ++ pr_non_empty_arg (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) -> |