Commit 476e5ea1 authored by POTTIER Francois's avatar POTTIER Francois

Remove the dynamic check in [KitCopy].

parent ccce10b5
......@@ -19,9 +19,10 @@ 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 check at runtime that this is
the case; however, only the domain check can be efficiently implemented. *)
assert (not (Atom.Map.mem x env));
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