diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-08-22 14:30:01 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-08-22 14:30:01 +0000 |
| commit | f6d8fc17dc9474e4d043cf709d672d9259599354 (patch) | |
| tree | 3e05dce982c2bebb63f432064136d927a227e0c7 /pretyping/namegen.ml | |
| parent | 08e7ec2c48c5ca666ad42b5f969576e6aa43d2ea (diff) | |
Nicer code concerning dirpaths and modpath around Lib
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16727 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/namegen.ml')
| -rw-r--r-- | pretyping/namegen.ml | 18 |
1 files changed, 8 insertions, 10 deletions
diff --git a/pretyping/namegen.ml b/pretyping/namegen.ml index a2fa81750..1736bcff2 100644 --- a/pretyping/namegen.ml +++ b/pretyping/namegen.ml @@ -26,16 +26,14 @@ open Termops (**********************************************************************) (* Globality of identifiers *) -let is_imported_modpath mp = - let current_mp,_ = Lib.current_prefix() in - match mp with - | MPfile dp -> - let rec find_prefix = function - |MPfile dp1 -> not (DirPath.equal dp1 dp) - |MPdot(mp,_) -> find_prefix mp - |MPbound(_) -> false - in find_prefix current_mp - | p -> false +let is_imported_modpath = function + | MPfile dp -> + let rec find_prefix = function + |MPfile dp1 -> not (DirPath.equal dp1 dp) + |MPdot(mp,_) -> find_prefix mp + |MPbound(_) -> false + in find_prefix (Lib.current_mp ()) + | _ -> false let is_imported_ref = function | VarRef _ -> false |