Comment typo fixed.

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index 563c8818670507e8844a183e9a3b184065319127..bf2918593fb04b63a4058befa1b334c072b5c93e 100644 (file)
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -47,9 +47,9 @@ let htmlfooter =
  "</html>"
 ;;
 
-let prooffile = "/public/sacerdot/currentproof";;
+let prooffile = "/home/galata/miohelm/currentproof";;
 (*CSC: the getter should handle the innertypes, not the FS *)
-let innertypesfile = "/public/sacerdot/innertypes";;
+let innertypesfile = "/home/galata/miohelm/innertypes";;
 
 (* GLOBAL REFERENCES (USED BY CALLBACKS) *)
 
@@ -248,7 +248,7 @@ prerr_endline ("Offending sequent: " ^ SequentPp.TextualPp.print_sequent current
 
 (*
 ignore(domImpl#saveDocumentToFile ~doc:sequent_doc
- ~name:"/public/sacerdot/guruguru1" ~indent:true ()) ;
+ ~name:"/home/galata/miohelm/guruguru1" ~indent:true ()) ;
 *)
 
 let mml_of_cic_term metano term =