lazy proof term to increase sharing and decrease memory consumption.

[helm.git] / helm / software / matita / matitaScript.ml

diff --git a/helm/software/matita/matitaScript.ml b/helm/software/matita/matitaScript.ml
index f769484c87706e9d615a7f9aa508b5ba1d9430db..a92b5b789707020df7c05b9de48ed906693cfe66 100644 (file)
--- 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;