diff options
Diffstat (limited to 'plugins/ltac/pptactic.ml')
| -rw-r--r-- | plugins/ltac/pptactic.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index 7fe17ceb7..d8bd16620 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -664,14 +664,14 @@ let pr_goal_selector ~toplevel s = let names = List.fold_left (fun ln (nal,_) -> List.fold_left - (fun ln na -> match na with (_,Name id) -> id::ln | _ -> ln) + (fun ln na -> match na with (_,Name id) -> Id.Set.add id ln | _ -> ln) ln nal) - [] bll in + Id.Set.empty bll in let idarg,bll = set_nth_name names n bll in - let annot = match names with - | [_] -> + let annot = + if Int.equal (Id.Set.cardinal names) 1 then mt () - | _ -> + else spc() ++ str"{" ++ keyword "struct" ++ spc () ++ pr_id idarg ++ str"}" |