snapshot, notably:

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

diff --git a/helm/matita/matitaInterpreter.ml b/helm/matita/matitaInterpreter.ml
index 511a5931476f30fe354246257fb7bf4665263fb8..bb43d67e0ae950159bb249a45d09262cb46bbaff 100644 (file)
--- a/helm/matita/matitaInterpreter.ml
+++ b/helm/matita/matitaInterpreter.ml
@@ -254,10 +254,6 @@ let inddef_of_ast params indTypes (disambiguator:MatitaTypes.disambiguator) =
       [] indTypes
   in
   let cicIndTypes = List.rev cicIndTypes in
-(*
-  prerr_endline uri;
-  pp_indtypes cicIndTypes;
-*)
   (UriManager.uri_of_string uri, (cicIndTypes, [], paramsno))
 
   (* TODO Zack a lot more to be done here:
@@ -423,7 +419,9 @@ class proofState
     | _ ->
         MatitaTypes.not_implemented "some tactic"
   in
-  let shared = new sharedState ~disambiguator ~currentProof ~console ~dbd () in
+  let shared =
+    new sharedState ~disambiguator ~currentProof ~console ?mathViewer ~dbd ()
+  in
   object (self)
     inherit interpreterState ~console