Merge PR #1040: Efficient fresh name generation

1 files changed, 5 insertions, 5 deletions

diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index f4e3ba633f..8a0764975d 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -662,14 +662,14 @@ type 'a extra_genarg_printer =
         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"}"