- coqc : option -image

- coqmktop : manquaient des -I
- tauto : rétablissement du vieux tauto en attendant la stabilité du nouveau
- correction d'un bug de Simpl avec Fix (découvert dans preuve FTA)


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1304 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 12 insertions, 14 deletions

diff --git a/scripts/coqc.ml b/scripts/coqc.ml
index 4dc09bc185..e93008b5f9 100644
--- a/scripts/coqc.ml
+++ b/scripts/coqc.ml
@@ -19,6 +19,7 @@ let environment = Unix.environment ()
 
 let bindir = ref Coq_config.bindir
 let binary = ref ("coqtop." ^ Coq_config.best)
+let image = ref ""
 
 (* the $COQBIN environment variable has priority over the Coq_config value *)
 let _ = 
@@ -122,8 +123,12 @@ let parse_args () =
 	binary := "coqtop.byte"; parse (cfiles,args) rem
     | "-opt" :: rem ->
 	binary := "coqtop.opt"; parse (cfiles,args) rem
+    | "-image" :: f :: rem ->
+	image := f; parse (cfiles,args) rem
+    | "-image" :: [] ->
+	usage ()
     | ("-?"|"-h"|"-H"|"-help"|"--help") :: _ -> usage ()
-    | ("-image"|"-libdir"|"-I"|"-include"|"-outputstate"
+    | ("-libdir"|"-I"|"-include"|"-outputstate"
       |"-inputstate"|"-is"|"-load-vernac-source"|"-load-vernac-object"
       |"-load-ml-source"|"-require"|"-load-ml-object"|"-user"
       |"-init-file" as o) :: rem ->
@@ -164,7 +169,9 @@ let main () =
     prerr_endline "coqc: too few arguments" ;
     usage ()
   end;
-  let coqtopname = Filename.concat !bindir !binary in
+  let coqtopname = 
+    if !image <> "" then !image else Filename.concat !bindir !binary 
+  in
   List.iter (compile coqtopname args) cfiles
     
 let _ = Printexc.print main (); exit 0
diff --git a/scripts/coqmktop.ml b/scripts/coqmktop.ml
index 0723aec671..9cafd5f7f3 100644
--- a/scripts/coqmktop.ml
+++ b/scripts/coqmktop.ml
@@ -58,20 +58,12 @@ let top        = ref false
 let searchisos = ref false
 let echo       = ref false
 
+let src_dirs = [ []; [ "config" ]; [ "toplevel" ] ]
+
 let includes () = 
   List.fold_right
     (fun d l -> "-I" :: List.fold_left Filename.concat !src_coqtop d :: l)
-    [ [ "config" ] ;
-      [ "scripts" ] ;
-      [ "lib" ] ;
-      [ "kernel" ] ;
-      [ "library" ] ;
-      [ "pretyping" ] ;
-      [ "parsing" ] ;
-      [ "proofs" ] ;
-      [ "tactics" ] ;
-      [ "toplevel" ]
-    ]
+    src_dirs
     ["-I"; Coq_config.camlp4lib]
 
 (* Transform bytecode object file names in native object file names *)
@@ -113,7 +105,6 @@ let all_subdirs dir =
   let l = ref [] in
   let add f = l := f :: !l in
   let rec traverse dir =
-    Printf.printf "%s\n" dir;
     let dirh = 
       try opendir dir with Unix_error _ -> invalid_arg "all_subdirs" 
     in