mathQL modified, stderr corrected to stdout im mathql_interpreter,

[helm.git] / helm / gTopLevel / gTopLevel.ml

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index d052040c5f8177502ac4e2a4c1cee1cb879cf3ea..85e9b5ebca09a87820decebc68f8b4fd3484ba29 100644 (file)
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -151,7 +151,7 @@ let mml_of_cic_object uri annobj ids_to_inner_sorts ids_to_inner_types =
 (*CSC: We save the innertypes to disk so that we can retrieve them in the  *)
 (*CSC: stylesheet. This DOES NOT work when UWOBO and/or the getter are not *)
 (*CSC: local.                                                              *)
-   Xml.pp xmlinnertypes (Some "/public/sacerdot/innertypes") ;
+   Xml.pp xmlinnertypes (Some "/home/fguidi/innertypes") ;
    let output = applyStylesheets input mml_styles mml_args in
     output
 ;;
@@ -1093,10 +1093,10 @@ let backward rendering_window () =
        match !ProofEngine.goal with
           | None -> ""
           | Some metano ->
-             let (_,_,ty) =
+             let (_, ey ,ty) =
               List.find (function (m,_,_) -> m=metano) metasenv
              in
-              MQueryGenerator.backward ty level
+              MQueryGenerator.backward metasenv ey ty level
        in 
    output_html outputhtml result