Fix Search is:Scheme

Fix coq#18298

tactics/declareScheme.ml

@@ -43,4 +43,4 @@ let declare_scheme kind indcl =
 
 let lookup_scheme kind ind = CString.Map.find kind (Indmap.find ind !scheme_map)
 
-let all_schemes () = Indmap.domain !scheme_map
+let all_schemes () = !scheme_map

tactics/declareScheme.mli

@@ -8,6 +8,8 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-val declare_scheme : string -> (Names.inductive * Names.Constant.t) -> unit
-val lookup_scheme : string -> Names.inductive -> Names.Constant.t
-val all_schemes : unit -> Names.Indset.t
+open Names
+
+val declare_scheme : string -> (inductive * Constant.t) -> unit
+val lookup_scheme : string -> inductive -> Constant.t
+val all_schemes : unit -> Constant.t CString.Map.t Indmap.t

vernac/comSearch.ml

@@ -45,7 +45,15 @@ let kind_searcher = Decls.(function
     Inr (fun gr -> List.exists (fun c -> GlobRef.CanOrd.equal c.Structures.CSTable.solution gr) canonproj)
   | IsDefinition Scheme ->
     let schemes = DeclareScheme.all_schemes () in
-    Inr (fun gr -> Indset.exists (fun c -> GlobRef.CanOrd.equal (GlobRef.IndRef c) gr) schemes)
+    let schemes = lazy begin
+      Indmap.fold (fun _ schemes acc ->
+          CString.Map.fold (fun _ c acc -> Cset.add c acc) schemes acc)
+        schemes Cset.empty
+    end
+    in
+    Inr (function
+        | ConstRef c -> Cset.mem c (Lazy.force schemes)
+        | _ -> false)
   | IsDefinition Instance ->
     let instances = Typeclasses.all_instances () in
     Inr (fun gr -> List.exists (fun c -> GlobRef.CanOrd.equal c.Typeclasses.is_impl gr) instances))