From afceace455a4b37ced7e29175ca3424996195f7b Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 14 Nov 2017 22:36:47 +0100 Subject: [api] Rename `global_reference` to `GlobRef.t` to follow kernel style. In #6092, `global_reference` was moved to `kernel`. It makes sense to go further and use the current kernel style for names. This has a good effect on the dependency graph, as some core modules don't depend on library anymore. A question about providing equality for the GloRef module remains, as there are two different notions of equality for constants. In that sense, `KerPair` seems suspicious and at some point it should be looked at. --- vernac/search.ml | 11 +++++------ 1 file changed, 5 insertions(+), 6 deletions(-) (limited to 'vernac/search.ml') diff --git a/vernac/search.ml b/vernac/search.ml index a2a4fb40f..6d07187fe 100644 --- a/vernac/search.ml +++ b/vernac/search.ml @@ -22,8 +22,8 @@ open Nametab module NamedDecl = Context.Named.Declaration -type filter_function = global_reference -> env -> constr -> bool -type display_function = global_reference -> env -> constr -> unit +type filter_function = GlobRef.t -> env -> constr -> bool +type display_function = GlobRef.t -> env -> constr -> unit (* This option restricts the output of [SearchPattern ...], [SearchAbout ...], etc. to the names of the symbols matching the @@ -61,7 +61,7 @@ let iter_named_context_name_type f = List.iter (fun decl -> f (NamedDecl.get_id decl) (NamedDecl.get_type decl)) (* General search over hypothesis of a goal *) -let iter_hypothesis glnum (fn : global_reference -> env -> constr -> unit) = +let iter_hypothesis glnum (fn : GlobRef.t -> env -> constr -> unit) = let env = Global.env () in let iter_hyp idh typ = fn (VarRef idh) env typ in let evmap,e = Pfedit.get_goal_context glnum in @@ -69,7 +69,7 @@ let iter_hypothesis glnum (fn : global_reference -> env -> constr -> unit) = iter_named_context_name_type iter_hyp pfctxt (* General search over declarations *) -let iter_declarations (fn : global_reference -> env -> constr -> unit) = +let iter_declarations (fn : GlobRef.t -> env -> constr -> unit) = let env = Global.env () in let iter_obj (sp, kn) lobj = match object_tag lobj with | "VARIABLE" -> @@ -117,8 +117,7 @@ module ConstrPriority = struct (* The priority is memoised here. Because of the very localised use of this module, it is not worth it making a convenient interface. *) - type t = - Globnames.global_reference * Environ.env * Constr.t * priority + type t = GlobRef.t * Environ.env * Constr.t * priority and priority = int module ConstrSet = CSet.Make(Constr) -- cgit v1.2.3