diff options
| author | Emilio Jesus Gallego Arias | 2019-06-21 22:50:08 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-07-08 15:59:10 +0200 |
| commit | c51fb2fae0e196012de47203b8a71c61720d6c5c (patch) | |
| tree | e49c2d38b6c841dc6514944750d21ed08ab94bce /plugins/syntax/numeral.ml | |
| parent | 437063a0c745094c5693d1c5abba46ce375d69c6 (diff) | |
[api] Deprecate GlobRef constructors.
Not pretty, but it had to be done some day, as `Globnames` seems to be
on the way out.
I have taken the opportunity to reduce the number of `open` in the
codebase.
The qualified style would indeed allow us to use a bit nicer names
`GlobRef.Inductive` instead of `IndRef`, etc... once we have the
tooling to do large-scale refactoring that could be tried.
Diffstat (limited to 'plugins/syntax/numeral.ml')
| -rw-r--r-- | plugins/syntax/numeral.ml | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/plugins/syntax/numeral.ml b/plugins/syntax/numeral.ml index 0a1cc8745d..a148a3bc73 100644 --- a/plugins/syntax/numeral.ml +++ b/plugins/syntax/numeral.ml @@ -12,7 +12,6 @@ open Pp open Util open Names open Libnames -open Globnames open Constrexpr open Constrexpr_ops open Notation @@ -31,7 +30,7 @@ let get_constructors ind = let mib,oib = Global.lookup_inductive ind in let mc = oib.Declarations.mind_consnames in Array.to_list - (Array.mapi (fun j c -> ConstructRef (ind, j + 1)) mc) + (Array.mapi (fun j c -> GlobRef.ConstructRef (ind, j + 1)) mc) let qualid_of_ref n = n |> Coqlib.lib_ref |> Nametab.shortest_qualid_of_global Id.Set.empty @@ -40,7 +39,7 @@ let q_option () = qualid_of_ref "core.option.type" let unsafe_locate_ind q = match Nametab.locate q with - | IndRef i -> i + | GlobRef.IndRef i -> i | _ -> raise Not_found let locate_z () = @@ -166,7 +165,7 @@ let vernac_numeral_notation local ty f g scope opts = { pt_local = local; pt_scope = scope; pt_interp_info = NumeralNotation o; - pt_required = Nametab.path_of_global (IndRef tyc),[]; + pt_required = Nametab.path_of_global (GlobRef.IndRef tyc),[]; pt_refs = constructors; pt_in_match = true } in |