Now "only" constraint are more restrictive.

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

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index 60d0d344b53b8c913a93efd420dcea9418cdf8f2..89e56bafc266310c0335985d7f61c19d95cc8b4d 100644 (file)
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -60,8 +60,8 @@ let htmlfooter =
  "</html>"
 ;;
 
-let prooffile = "/public/sacerdot/currentproof";;
-let prooffiletype = "/public/sacerdot/currentprooftype";;
+let prooffile = "/public/natile/currentproof";;
+let prooffiletype = "/public/natile/currentprooftype";;
 
 (* SACERDOT
 let prooffile = "/public/sacerdot/currentproof";;
@@ -85,8 +85,8 @@ let prooffiletype = "/home/galata/miohelm/currentprooftype";;
 
 (*CSC: the getter should handle the innertypes, not the FS *)
 
-let innertypesfile = "/public/sacerdot/innertypes";;
-let constanttypefile = "/public/sacerdot/constanttype";;
+let innertypesfile = "/public/natile/innertypes";;
+let constanttypefile = "/public/natile/constanttype";;
 
 (* SACERDOT
 let innertypesfile = "/public/sacerdot/innertypes";;