diff options
Diffstat (limited to 'printing/pptactic.ml')
| -rw-r--r-- | printing/pptactic.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/printing/pptactic.ml b/printing/pptactic.ml index 4cb7e9fb38..50a543968a 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -1201,7 +1201,7 @@ module Make | TacML (loc,s,l) -> pr_with_comments loc (pr.pr_extend 1 s l), lcall | TacAlias (loc,kn,l) -> - pr_with_comments loc (pr.pr_alias (level_of inherited) kn (List.map snd l)), latom + pr_with_comments loc (pr.pr_alias (level_of inherited) kn l), latom ) in if prec_less prec inherited then strm |