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/extraction/extract_env.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/extraction/extract_env.ml')
| -rw-r--r-- | plugins/extraction/extract_env.ml | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index ca1520594d..551dbdc6fb 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -14,7 +14,6 @@ open Declarations open Names open ModPath open Libnames -open Globnames open Pp open CErrors open Util @@ -118,7 +117,7 @@ module Visit : VISIT = struct v.mp <- MPset.union (prefixes_mp mp) v.mp; v.mp_all <- MPset.add mp v.mp_all let add_kn kn = v.kn <- KNset.add kn v.kn; add_mp (KerName.modpath kn) - let add_ref = function + let add_ref = let open GlobRef in function | ConstRef c -> add_kn (Constant.user c) | IndRef (ind,_) | ConstructRef ((ind,_),_) -> add_kn (MutInd.user ind) | VarRef _ -> assert false @@ -761,7 +760,7 @@ let show_extraction ~pstate = let ast, ty = extract_constr env sigma t in let mp = Lib.current_mp () in let l = Label.of_id (Proof_global.get_proof_name pstate) in - let fake_ref = ConstRef (Constant.make2 mp l) in + let fake_ref = GlobRef.ConstRef (Constant.make2 mp l) in let decl = Dterm (fake_ref, ast, ty) in print_one_decl [] mp decl in |