From 223c86e91a4c5dceb8bdacf411f47c43d69a5dd0 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 29 Nov 2020 13:18:00 +0100
Subject: Fixing printing of apply in (continuation of #12246).

---
 plugins/ltac/pptactic.ml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'plugins/ltac')

diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index fa5bbf7676..a7773686af 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -458,7 +458,8 @@ let string_of_genarg_arg (ArgumentType arg) =
     | l -> pr_in (spc () ++ prlist_with_sep spc pr_id l)
 
   let pr_in_hyp_as prc pr_id = function
-    | (id,ipat) -> pr_in (spc () ++ pr_id id) ++ pr_as_ipat prc ipat
+    | [] -> mt ()
+    | l -> pr_in (spc () ++ prlist_with_sep pr_comma (fun (id,ipat) -> pr_id id ++ pr_as_ipat prc ipat) l)
 
   let pr_in_clause pr_id = function
     | { onhyps=None; concl_occs=NoOccurrences } ->
@@ -755,7 +756,7 @@ let pr_goal_selector ~toplevel s =
             (if a then mt() else primitive "simple ") ++
               primitive (with_evars ev "apply") ++ spc () ++
               prlist_with_sep pr_comma pr_with_bindings_arg cb ++
-              prlist_with_sep spc (pr_in_hyp_as (pr.pr_dconstr env sigma) pr.pr_name) inhyp
+              pr_non_empty_arg (pr_in_hyp_as (pr.pr_dconstr env sigma) pr.pr_name) inhyp
           )
         | TacElim (ev,cb,cbo) ->
           hov 1 (
-- 
cgit v1.2.3