From 6da8866a4fd79029b22bd1bf7cde6725a9ea259c Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 16 Apr 2016 16:45:44 +0200
Subject: Fixing printing of inversion as.

---
 printing/pptactic.ml | 8 ++++----
 1 file 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) ->
-- 
cgit v1.2.3