--- Makefile.in.orig	2018-01-23 03:07:35.000000000 -0700
+++ Makefile.in	2018-02-10 15:44:26.226883183 -0700
@@ -155,7 +155,7 @@ CMO_EXPORT =  src/lib.cmo src/rc.cmo src
 	   src/effect.cmo src/pp.cmo src/option_misc.cmo \
 	   src/report.cmo \
            src/explain.cmo 	\
-	   src/xml.cmo src/project.cmo
+	   src/xml.cmo src/whyproject.cmo
 
 # jessie
 JCCML_EXPORT = src/why3_kw.ml jc/output.ml \
--- src/options.mli.orig	2018-01-23 03:07:35.000000000 -0700
+++ src/options.mli	2018-02-10 15:44:26.258883112 -0700
@@ -184,7 +184,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	2018-01-23 03:07:35.000000000 -0700
+++ src/pretty.ml	2018-02-10 15:44:26.259883110 -0700
@@ -416,12 +416,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 ->
@@ -431,15 +431,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	2018-01-23 03:07:35.000000000 -0700
+++ src/pretty.mli	2018-02-10 15:44:26.259883110 -0700
@@ -50,4 +50,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	2018-01-23 03:07:35.000000000 -0700
+++ src/whyweb.ml	2018-02-10 15:44:26.259883110 -0700
@@ -29,7 +29,7 @@
 (**************************************************************************)
 
 open Format
-open Project
+open Whyproject
 
 (*prover*)
 let provers = [Ergo ; Simplify ; Z3 ; Yices ; Cvc3]
@@ -168,7 +168,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 ""
 
@@ -260,7 +260,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 -> Whyproject.save !proj !proj.project_name
     end;
     loc
   with Not_found -> ("",0,0,0)
@@ -343,7 +343,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 _ -> 
@@ -526,7 +526,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>
 ";