From 72c9850370ab0e0b02b3d49a837dd442410f8ba6 Mon Sep 17 00:00:00 2001 From: =?utf8?q?Michele=20Galat=C3=A0?= Date: Thu, 29 Aug 2002 13:18:34 +0000 Subject: [PATCH] Comment typo fixed. --- helm/gTopLevel/gTopLevel.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index 563c88186..bf2918593 100644 --- a/helm/gTopLevel/gTopLevel.ml +++ b/helm/gTopLevel/gTopLevel.ml @@ -47,9 +47,9 @@ let htmlfooter = "" ;; -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 = -- 2.39.2