Commit 90958d5d authored by Guillaume Melquiond's avatar Guillaume Melquiond

Lazily load references to constants inside the Coq tactic.

parent 6b4e99f7
......@@ -99,6 +99,16 @@ let map_to_list = CArray.map_to_list
let force x = x
let coq_reference t1 t2 =
let th = lazy (coq_reference t1 t2) in
fun x -> lazy (Lazy.force th x)
let find_reference t1 t2 =
let th = lazy (find_reference t1 t2) in
fun x -> lazy (Lazy.force th x)
let is_global c t = is_global (Lazy.force c) t
DECLARE PLUGIN "why3tac"
END
......
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