X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FmatitaAutoGui.ml;h=588dc5fecd09363f7de821a80eecb261ed083624;hb=1439ced76cb62f9c5f5e638c53a005c3843870ae;hp=d01cac5d14a698166a25637fcd379f0aadc4c9f7;hpb=02763a89e6351dfb7770251d0507512e3f0ddb74;p=helm.git

diff --git a/helm/software/matita/matitaAutoGui.ml b/helm/software/matita/matitaAutoGui.ml
index d01cac5d1..588dc5fec 100644
--- a/helm/software/matita/matitaAutoGui.ml
+++ b/helm/software/matita/matitaAutoGui.ml
@@ -25,9 +25,9 @@
  *)
 
 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 = [];;
 
@@ -57,16 +57,16 @@ let pp ?(size=(!font_size)) c t =
 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 =