Commit 95476c03 authored by POTTIER Francois's avatar POTTIER Francois

Remove a runtime check in [KitExport].

parent de5fa033
......@@ -4,8 +4,6 @@
(* The environment is an injective mapping of atoms to strings. We keep track
of its codomain by recording a mapping of hints to integers. *)
(* TEMPORARY move the low-level code to [Atom]? *)
module StringMap =
......@@ -26,8 +24,6 @@ let next env hint : int =
let extend x env =
(* Under the GUH, the atom [x] cannot appear in the domain of [env]. *)
assert (not (Atom.Map.mem x env.graph));
(* We must pick a suitable string to stand for the atom [x]. We must
pick a string that does not appear in the image through [env] of
the free atoms of [body]. However, at this point, we do not have
......@@ -51,6 +47,7 @@ let lookup env a =
with Not_found ->
(* The atom [a] must be in the domain of [env]. *)
assert false
(* Instead of failing, we could also log an error and return "?". *)
class ['self] map = object (_ : 'self)
method private extend = extend
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