X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=helm%2Fmatita%2FmatitaInterpreter.ml;h=e578a3eb039a44612b163b0f422b216c258ebbc3;hb=fdd8107cc53f5e862004aa5fcd48593ee5634234;hp=9440e84665daa25ed676560ce0a999e9b1f58f4d;hpb=ab336f7c09d052c45a09dd49e9b75a39e8b57e5b;p=helm.git

diff --git a/helm/matita/matitaInterpreter.ml b/helm/matita/matitaInterpreter.ml
index 9440e8466..e578a3eb0 100644
--- a/helm/matita/matitaInterpreter.ml
+++ b/helm/matita/matitaInterpreter.ml
@@ -139,10 +139,10 @@ class sharedState
             !(Lazy.force basedir));
           Quiet
       | TacticAst.Command (TacticAst.Check term) ->
-          let (_, _, term,ugraph) = 
+          let (_, metasenv, term,ugraph) = 
 	    MatitaCicMisc.disambiguate ~disambiguator ~currentProof term 
 	  in
-          let (context, metasenv) =
+          let (context, _) =
             MatitaCicMisc.get_context_and_metasenv currentProof
           in
 (* this is the Eval Compute
@@ -155,7 +155,7 @@ class sharedState
 	    (* TASSI: here ugraph1 is unused.... FIXME *)
           let expr = Cic.Cast (term, ty) in
           (match mathViewer with
-          | Some v -> v#checkTerm (`Cic expr)
+          | Some v -> v#checkTerm (`Cic (expr, metasenv))
           | _ -> ());
           Quiet
       | TacticAst.Command (TacticAst.Search_pat (search_kind, pat)) ->