diff options
| author | Pierre-Marie Pédrot | 2020-11-29 17:29:15 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-11-29 17:29:15 +0100 |
| commit | ca8ee04a692e14bd90c64113ff29b7df1d5111bd (patch) | |
| tree | f5149acae95edbd1baf8de064bb716f4e84cd5f2 /plugins | |
| parent | 9992bb15d4f90fc0cf3aa2854beb209bc5effac6 (diff) | |
| parent | 223c86e91a4c5dceb8bdacf411f47c43d69a5dd0 (diff) | |
Merge PR #13514: Fixing printing of apply in (continuation of #12246)
Reviewed-by: ppedrot
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/ltac/pptactic.ml | 5 |
1 files changed, 3 insertions, 2 deletions
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 ( |