Merge PR #12531: Fast inductive compilation

Reviewed-by: SkySkimmer

1 files changed, 17 insertions, 12 deletions

diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index 95489c9132..e490b33dde 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -60,23 +60,28 @@ type structured_one_inductive_expr = {
   ind_lc : (Id.t * constr_expr) list
 }
 
+exception Same of Id.t
+
 let check_all_names_different indl =
+  let rec elements = function
+  | [] -> Id.Set.empty
+  | id :: l ->
+    let s = elements l in
+    if Id.Set.mem id s then raise (Same id) else Id.Set.add id s
+  in
   let ind_names = List.map (fun ind -> ind.ind_name) indl in
   let cstr_names = List.map_append (fun ind -> List.map fst ind.ind_lc) indl in
-  let l = List.duplicates Id.equal ind_names in
-  let () = match l with
-  | [] -> ()
-  | t :: _ -> raise (InductiveError (SameNamesTypes t))
+  let ind_names = match elements ind_names with
+  | s -> s
+  | exception (Same t) -> raise (InductiveError (SameNamesTypes t))
   in
-  let l = List.duplicates Id.equal cstr_names in
-  let () = match l with
-  | [] -> ()
-  | c :: _ -> raise (InductiveError (SameNamesConstructors (List.hd l)))
+  let cstr_names = match elements cstr_names with
+  | s -> s
+  | exception (Same c) -> raise (InductiveError (SameNamesConstructors c))
   in
-  let l = List.intersect Id.equal ind_names cstr_names in
-  match l with
-  | [] -> ()
-  | _ -> raise (InductiveError (SameNamesOverlap l))
+  let l = Id.Set.inter ind_names cstr_names in
+  if not (Id.Set.is_empty l) then
+    raise (InductiveError (SameNamesOverlap (Id.Set.elements l)))
 
 (** Make the arity conclusion flexible to avoid generating an upper bound universe now,
     only if the universe does not appear anywhere else.