diff --git a/tactics/declareScheme.ml b/tactics/declareScheme.ml index 98507d91ee211..a9568dc556b5a 100644 --- a/tactics/declareScheme.ml +++ b/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 diff --git a/tactics/declareScheme.mli b/tactics/declareScheme.mli index 3a8f8ee2e2006..08a5a52cf6fa2 100644 --- a/tactics/declareScheme.mli +++ b/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 diff --git a/vernac/comSearch.ml b/vernac/comSearch.ml index b0e3a114eae8c..b16154be2f85e 100644 --- a/vernac/comSearch.ml +++ b/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))