diff options
author | 2013-09-19 17:37:21 +0000 | |
---|---|---|
committer | 2013-09-19 17:37:21 +0000 | |
commit | efae3184752f19a6cfb95b05ad42438c87ee3a9e (patch) | |
tree | 055e4e67f22badc405252b7f84894ff63d1ce054 | |
parent | 736ffcea3a04da40ea3047216864ca420f220fe5 (diff) |
Prettyp: avoid useless "let module"
As hinted by X. Clerc, a "let module" induces some runtime cost,
so let's try to avoid them when possible.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16789 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r-- | printing/prettyp.ml | 19 |
1 files changed, 8 insertions, 11 deletions
diff --git a/printing/prettyp.ml b/printing/prettyp.ml index 0e0480836..5066a7b6e 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -23,7 +23,6 @@ open Impargs open Libobject open Libnames open Globnames -open Nametab open Recordops open Misctypes open Printer @@ -286,15 +285,14 @@ type logical_name = | Undefined of qualid let locate_any_name ref = - let module N = Nametab in let (loc,qid) = qualid_of_reference ref in - try Term (N.locate qid) + try Term (Nametab.locate qid) with Not_found -> - try Syntactic (N.locate_syndef qid) + try Syntactic (Nametab.locate_syndef qid) with Not_found -> - try Dir (N.locate_dir qid) + try Dir (Nametab.locate_dir qid) with Not_found -> - try ModuleType (qid, N.locate_modtype qid) + try ModuleType (qid, Nametab.locate_modtype qid) with Not_found -> Undefined qid let pr_located_qualid = function @@ -323,13 +321,12 @@ let pr_located_qualid = function let print_located_qualid ref = let (loc,qid) = qualid_of_reference ref in - let module N = Nametab in let expand = function | TrueGlobal ref -> - Term ref, N.shortest_qualid_of_global Id.Set.empty ref + Term ref, Nametab.shortest_qualid_of_global Id.Set.empty ref | SynDef kn -> - Syntactic kn, N.shortest_qualid_of_syndef Id.Set.empty kn in - match List.map expand (N.locate_extended_all qid) with + Syntactic kn, Nametab.shortest_qualid_of_syndef Id.Set.empty kn in + match List.map expand (Nametab.locate_extended_all qid) with | [] -> let (dir,id) = repr_qualid qid in if DirPath.is_empty dir then @@ -652,7 +649,7 @@ let print_name = function let print_opaque_name qid = let env = Global.env () in - match global qid with + match Nametab.global qid with | ConstRef cst -> let cb = Global.lookup_constant cst in if Declareops.constant_has_body cb then |