X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaMathView.ml;h=59324f1a1fe04e9de6e348f72f638cb3e194fb92;hb=fdd8107cc53f5e862004aa5fcd48593ee5634234;hp=7aa54f2c74ed03a3407bc4b4d18e5165f67c6da3;hpb=393b5943416585d0612ec62b795ceee34adb8dd7;p=helm.git

diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml
index 7aa54f2c7..59324f1a1 100644
--- 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")