diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-08-04 21:29:41 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-08-04 21:29:41 +0000 |
| commit | ff0a77ae90f39c56e82126978a59d957676e0d9e (patch) | |
| tree | 89df8f3f9f9c353e5ecede1a75278648baaec4c3 /pretyping | |
| parent | 7d515acbc5d83aa2300b71a9b7712b3da1d3d2e3 (diff) | |
Report des commits 11297 et 11299 (nom Unnamed_theorem local caché par
un nom importé) de la 8.2 vers le trunk.
--Cette ligne, et les suivantes ci-dessous, seront ignorées--
M pretyping/termops.ml
M toplevel/command.ml
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11302 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/termops.ml | 15 |
1 files changed, 4 insertions, 11 deletions
diff --git a/pretyping/termops.ml b/pretyping/termops.ml index c0144cab4..f0a781cf0 100644 --- a/pretyping/termops.ml +++ b/pretyping/termops.ml @@ -817,29 +817,22 @@ let names_of_rel_context env = (**** Globality of identifiers *) -(* TODO temporary hack!!! *) let rec is_imported_modpath = function - | MPfile dp -> dp <> (Lib.library_dp ()) -(* | MPdot (mp,_) -> is_imported_modpath mp *) - | _ -> false + | MPfile dp -> true + | p -> false let is_imported_ref = function | VarRef _ -> false | IndRef (kn,_) - | ConstructRef ((kn,_),_) -(* | ModTypeRef ln *) -> + | ConstructRef ((kn,_),_) -> let (mp,_,_) = repr_kn kn in is_imported_modpath mp -(* | ModRef mp -> - is_imported_modpath mp -*) | ConstRef kn -> let (mp,_,_) = repr_con kn in is_imported_modpath mp let is_global id = try let ref = locate (make_short_qualid id) in - not (is_imported_ref ref) || - (try ignore(locate (make_qualid (dirpath_of_string "Top") id)); true with _ -> false) + not (is_imported_ref ref) with Not_found -> false |