diff options
| author | Hugo Herbelin | 2016-04-16 16:45:44 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2016-06-16 17:30:18 +0200 |
| commit | 364290af0983534c447fec9c5819bccf83a06453 (patch) | |
| tree | 9793ec9d4d5c701f78380b7abb8ba02f5fbb2ea1 | |
| parent | 164afe9ffbfdc74a567da3c8ba77b6ef8c848b23 (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 5711e6c4f2..370e1ac317 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -623,7 +623,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" @@ -951,16 +951,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) -> |