added a (for the moment) dummy field _subst to ProofengineTypes.proof.

[helm.git] / matita / matitaScript.ml

diff --git a/matita/matitaScript.ml b/matita/matitaScript.ml
index 9eb1dbf69c608c9ba231d4e46f45f3ae78fb1f18..fe8e691204800fb82d09cc5e3820a1896eae3361 100644 (file)
--- a/matita/matitaScript.ml
+++ b/matita/matitaScript.ml
@@ -226,7 +226,8 @@ let rec eval_macro include_paths (buffer : GText.buffer) guistuff lexicon_status
      guistuff.mathviewer#show_uri_list ~reuse:true ~entry l;
      [], "", parsed_text_length
   | TA.WHint (loc, term) ->
-     let s = ((None,[0,[],term], Cic.Meta (0,[]) ,term, []),0) in
+     let _subst = [] in
+     let s = ((None,[0,[],term], _subst, 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;