support for terms with metas in check

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)) ->

diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml
index 7aa54f2c74ed03a3407bc4b4d18e5165f67c6da3..59324f1a1fe04e9de6e348f72f638cb3e194fb92 100644 (file)
--- a/helm/matita/matitaMathView.ml
+++ b/helm/matita/matitaMathView.ml
@@ -431,13 +431,13 @@ class cicBrowser ~(history:string MatitaMisc.history) () =
       self#_loadTermAst (disambiguator#parserr#parseTerm (Stream.of_string s))
 
     method private _loadTermAst ast =
-      let (_, _, term, _) =
+      let (_, metasenv, term, _) =
         MatitaCicMisc.disambiguate ~disambiguator ~currentProof ast
       in
-      self#_loadTermCic term
+      self#_loadTermCic term metasenv
 
-    method private _loadTermCic term =
-      let (context, metasenv) =
+    method private _loadTermCic term metasenv =
+      let (context, _) =
         MatitaCicMisc.get_context_and_metasenv currentProof
       in
       let dummyno = CicMkImplicit.new_meta metasenv [] in
@@ -448,7 +448,7 @@ class cicBrowser ~(history:string MatitaMisc.history) () =
       handle_error (fun () ->
         (match src with
         | `Ast ast -> self#_loadTermAst ast
-        | `Cic cic -> self#_loadTermCic cic
+        | `Cic (cic, metasenv) -> self#_loadTermCic cic metasenv
         | `String s -> self#_loadTerm s);
         self#setUri "check")
 

diff --git a/helm/matita/matitaTypes.ml b/helm/matita/matitaTypes.ml
index 73a5da1a1c3bc863df34b0516c9724e0b709c09e..95618d142624e932493666da151773b8d9f412c5 100644 (file)
--- a/helm/matita/matitaTypes.ml
+++ b/helm/matita/matitaTypes.ml
@@ -160,7 +160,7 @@ class type interpreter =
 
 type term_source =
   [ `Ast of DisambiguateTypes.term
-  | `Cic of Cic.term
+  | `Cic of Cic.term * Cic.metasenv
   | `String of string
   ]
 

diff --git a/helm/matita/matitaTypes.mli b/helm/matita/matitaTypes.mli
index 1db5bb0de04ea2efb8454458d3da9b73d00f8478..26299967224cb6b4f850da5a53935360691296e9 100644 (file)
--- a/helm/matita/matitaTypes.mli
+++ b/helm/matita/matitaTypes.mli
@@ -198,7 +198,7 @@ class type interpreter =
 
 type term_source =
   [ `Ast of DisambiguateTypes.term
-  | `Cic of Cic.term
+  | `Cic of Cic.term * Cic.metasenv
   | `String of string
   ]