support for terms with metas in check

[helm.git] / helm / matita / matitaInterpreter.ml

diff --git a/helm/matita/matitaInterpreter.ml b/helm/matita/matitaInterpreter.ml
index 9440e84665daa25ed676560ce0a999e9b1f58f4d..e578a3eb039a44612b163b0f422b216c258ebbc3 100644 (file)
--- 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)) ->