*)
type status =
- Cic.context * (int * Cic.term * bool * int * (int * Cic.term) list) list *
+ Cic.context * (int * Cic.term * bool * int * (int * Cic.term Lazy.t) list) list *
(int * Cic.term * int) list *
- Cic.term list
+ Cic.term Lazy.t list
let fake_goal = Cic.Implicit None;;
let fake_candidates = [];;
let pp_goal context x =
if x == fake_goal then "" else pp context x
;;
-let pp_candidate context x = pp context x
-let pp_candidate_tip context x = pp ~size:0 context x
+let pp_candidate context x = pp context (Lazy.force x)
+let pp_candidate_tip context x = pp ~size:0 context (Lazy.force x)
let pp_candidate_type context x =
try
let ty, _ =
CicTypeChecker.type_of_aux' [] ~subst:[]
- context x CicUniv.oblivion_ugraph
+ context (Lazy.force x) CicUniv.oblivion_ugraph
in
pp ~size:0 context ty
- with CicUtil.Meta_not_found _ -> pp ~size:0 context x
+ with CicUtil.Meta_not_found _ -> pp ~size:0 context (Lazy.force x)
;;
let sublist start len l =