X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FmatitaScript.ml;h=a92b5b789707020df7c05b9de48ed906693cfe66;hb=7a29aa43eb607d019699f0a76dc83e7093e5b222;hp=f769484c87706e9d615a7f9aa508b5ba1d9430db;hpb=6a5e51c1cf9a56c74a8b53a9b8bc5aa686c9780e;p=helm.git diff --git a/helm/software/matita/matitaScript.ml b/helm/software/matita/matitaScript.ml index f769484c8..a92b5b789 100644 --- a/helm/software/matita/matitaScript.ml +++ b/helm/software/matita/matitaScript.ml @@ -440,7 +440,7 @@ let rec eval_macro include_paths (buffer : GText.buffer) guistuff lexicon_status [], "", parsed_text_length | TA.WHint (loc, term) -> let _subst = [] in - let s = ((None,[0,[],term], _subst, Cic.Meta (0,[]) ,term, []),0) in + let s = ((None,[0,[],term], _subst, lazy (Cic.Meta (0,[])) ,term, []),0) in let l = List.map fst (MQ.experimental_hint ~dbd s) in let entry = `Whelp (pp_macro mac, l) in guistuff.mathviewer#show_uri_list ~reuse:true ~entry l;