Commit 22f30ea5 authored by POTTIER Francois's avatar POTTIER Francois

Removed a comment on the GUH in KitCopy.

parent ff0b194f
......@@ -16,11 +16,6 @@ let lookup env x =
let extend x env =
(* Under the global uniqueness assumption, the atom [x] cannot appear in the
domain or codomain of the environment. We could check at runtime that this is
the case; however, only the domain check can be efficiently implemented.
Furthermore, we would like the [copy] function to be used for establishing
the GUH when it does not hold. So, we do not perform any runtime check. *)
(* Generate a fresh copy of [x]. *)
let x' = Atom.fresha x in
(* Extend [env] when descending in the body. *)
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