--- ./Makefile.in.orig	2014-03-17 16:01:46.000000000 -0600
+++ ./Makefile.in	2014-06-26 12:30:00.000000000 -0600
@@ -222,7 +222,7 @@ CMO_EXPORT =  src/lib.cmo src/rc.cmo src
 	   src/effect.cmo src/pp.cmo src/option_misc.cmo \
 	   src/parser.cmo src/lexer.cmo src/report.cmo \
            src/explain.cmo 	\
-	   src/xml.cmo src/project.cmo
+	   src/xml.cmo src/whyproject.cmo
 
 CMO = src/lib.cmo src/rc.cmo tools/dpConfig.cmo \
       src/version.cmo src/options.cmo src/linenum.cmo src/loc.cmo \
@@ -239,7 +239,7 @@ CMO = src/lib.cmo src/rc.cmo tools/dpCon
 	   src/holl.cmo src/harvey.cmo src/simplify.cmo  \
            src/regen.cmo src/mizar.cmo src/smtlib.cmo src/coq.cmo \
 	   src/zenon.cmo src/z3.cmo src/cvcl.cmo tools/calldp.cmo \
-	   src/xml.cmo src/project.cmo \
+	   src/xml.cmo src/whyproject.cmo \
 	   src/why3_kw.cmo src/why3.cmo src/pretty.cmo  \
            src/unionfind.cmo src/theoryreducer.cmo \
            src/theory_filtering.cmo src/hypotheses_filtering.cmo \
--- ./src/options.mli.orig	2014-03-17 16:01:46.000000000 -0600
+++ ./src/options.mli	2014-06-26 12:30:00.000000000 -0600
@@ -185,7 +185,7 @@ val files : string list
 (*s GUI? *)
 
 val gui : bool ref
-val gui_project : Project.t option ref
+val gui_project : Whyproject.t option ref
 val lib_files_to_load : string list
 
 (*
--- ./src/pretty.ml.orig	2014-03-17 16:01:46.000000000 -0600
+++ ./src/pretty.ml	2014-06-26 12:30:00.000000000 -0600
@@ -415,12 +415,12 @@ let output_project f =
        with Not_found ->
 	 functions := SMap.add fn SMap.empty !functions)
     Util.program_locs ;
-  let p = Project.create (Filename.basename f) in
-  Project.set_project_context_file p (f ^ "_ctx.why");
+  let p = Whyproject.create (Filename.basename f) in
+  Whyproject.set_project_context_file p (f ^ "_ctx.why");
   List.iter
     (fun (expl,fpo) ->
        let n = expl.lemma_or_fun_name in
-       let _ = Project.add_lemma p n expl fpo in ())
+       let _ = Whyproject.add_lemma p n expl fpo in ())
     !lemmas;
   SMap.iter
     (fun fname behs ->
@@ -430,15 +430,15 @@ let output_project f =
 	   floc
 	 with Not_found -> Loc.dummy_floc
        in
-       let f = Project.add_function p fname floc in
+       let f = Whyproject.add_function p fname floc in
        SMap.iter
 	 (fun beh vcs ->
-	    let be = Project.add_behavior f beh floc in
+	    let be = Whyproject.add_behavior f beh floc in
 	    List.iter
 	      (fun (expl,fpo) ->
-		 let _ = Project.add_goal be expl fpo in ())
+		 let _ = Whyproject.add_goal be expl fpo in ())
 	      vcs)
 	 behs)
     !functions;
-  Project.save p f;
+  Whyproject.save p f;
   p
--- ./src/pretty.mli.orig	2014-03-17 16:01:46.000000000 -0600
+++ ./src/pretty.mli	2014-06-26 12:30:00.000000000 -0600
@@ -51,4 +51,4 @@ val output_files : string -> unit
 (* [output_project f] produces a whole project description, in a file
 [f.wpr], together with other needed files [f_ctx.why], [f_lemmas.why],
 and each goal in a separate file [f_po<i>.why] for i=1,2,... *)
-val output_project : string -> Project.t
+val output_project : string -> Whyproject.t
--- ./src/whyweb.ml.orig	2014-03-17 16:01:46.000000000 -0600
+++ ./src/whyweb.ml	2014-06-26 12:30:00.000000000 -0600
@@ -30,7 +30,7 @@
 (**************************************************************************)
 
 open Format
-open Project
+open Whyproject
 
 (*prover*)
 let provers = [Ergo ; Simplify ; Z3 ; Yices ; Cvc3]
@@ -169,7 +169,7 @@ let file = match !file with
   | None -> ()
   | Some f -> Arg.usage spec usage; exit 1
 
-let proj = ref (Project.create "")
+let proj = ref (Whyproject.create "")
 
 let proj_file = ref ""
 
@@ -261,7 +261,7 @@ let interp_com c =
 	  let _ =  Thread.create (launch_behavior Cvc3)  b in ()
       | `LaunchCvc3Function f -> 
 	  let _ =  Thread.create (launch_function Cvc3) f  in ()
-      | `Save -> Project.save !proj !proj.project_name
+      | `Save -> Whyroject.save !proj !proj.project_name
     end;
     loc
   with Not_found -> ("",0,0,0)
@@ -344,7 +344,7 @@ let main_page msg =
 let load_prj file =
   eprintf "Reading file %s@." file;
   try
-    proj := Project.load file;
+    proj := Whyproject.load file;
     proj_file := file;
   with
       Sys_error _ -> 
@@ -527,7 +527,7 @@ wprint "<center><a href=\"%s\">Save Proj
 <table border=\"1\"  cellpadding=\"0\" cellspacing=\"0\">" ns;
 	 wprint "<tr><th></th>";
 	 List.iter (fun prover -> 
-		      wprint "<th>%s</th>" (Project.provers_name prover)) 
+		      wprint "<th>%s</th>" (Whyproject.provers_name prover)) 
 	   provers;
 	 wprint "</tr>
 ";