diff options
| author |  Pierre Courtieu <Pierre.Courtieu@cnam.fr> | 2017-05-02 21:32:26 +0200 |
|---|---|---|
| committer | Pierre Courtieu <Pierre.Courtieu@cnam.fr> | 2017-05-04 11:13:49 +0200 |
| commit | 8bcf71360261d789ac3ab919bc49309df678628f (patch) | |
| tree | 0bf128027766f3113e2b19686c1a065088ceb3fa /printing/printer.ml | |
| parent | 1fe73e6af81759fa8b78c8660745492ed886d477 (diff) | |
labelizing arguments
Diffstat (limited to 'printing/printer.ml')
| -rw-r--r-- | printing/printer.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/printing/printer.ml b/printing/printer.ml index 3d67e89f5..1d3e67d9d 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -688,7 +688,7 @@ let default_pr_subgoals ?(pr_first=true) let print_multiple_goals g l = if pr_first then default_pr_goal { it = g ; sigma = sigma; } - ++ (if l=[] then str"" else cut ()) + ++ (if l=[] then mt () else cut ()) ++ pr_rec 2 l else pr_rec 1 (g::l) |