Commit 3f5e6e1f authored by Andrei Paskevich's avatar Andrei Paskevich

Theory, Pmodule: imported names can shadow the locally declared ones

As we have to implement the "HERE" and "PARENT" qualifiers anyway,
allowing this shadowing lets us accept more programs without
compromising the "everything is unambigously nameable" invariant.
parent 8a1ecac1
(* test file *)
theory A
type t
end
theory B
type t
use import A
end
......@@ -313,7 +313,6 @@ let close_scope uc ~import =
match uc.uc_prefix, uc.uc_import, uc.uc_export with
| s :: prf, _ :: i1 :: sti, e0 :: e1 :: ste ->
let i1 = if import then merge_ns false e0 i1 else i1 in
let _ = if import then merge_ns true e0 e1 else e1 in
let i1 = add_ns false s e0 i1 in
let e1 = add_ns true s e0 e1 in
{ uc with uc_prefix = prf; uc_import = i1::sti; uc_export = e1::ste; }
......
......@@ -185,7 +185,6 @@ let close_scope uc ~import =
muc_import = sti; muc_export = ste; }
| Uscope (s,_,ul1) :: ul0, _ :: i1 :: sti, e0 :: e1 :: ste ->
let i1 = if import then merge_ns false e0 i1 else i1 in
let _ = if import then merge_ns true e0 e1 else e1 in
let i1 = add_ns false s e0 i1 in
let e1 = add_ns true s e0 e1 in
{ uc with
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment