diff options
| -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) -> |