- fixed the Assert_failure error in kernel/modops

- fixed the problem with passing atomic tactics to ltacs
- restructured the distrib Makefile (can build a package from
  the CVS working dir)


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

4 files changed, 20 insertions, 23 deletions

diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index 95e29fd218..5165abfd5a 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -12,16 +12,18 @@ open Pp
 open System
 open Toplevel
 
+let (/) = Filename.concat
+
 let set_debug () = Options.debug := true
 
 (* Loading of the ressource file.
    rcfile is either $HOME/.coqrc.VERSION, or $HOME/.coqrc if the first one
   does not exist. *)
 
-let rcfile = ref (Filename.concat home ".coqrc")
+let rcfile = ref (home/".coqrc")
 let rcfile_specified = ref false
 let set_rcfile s = rcfile := s; rcfile_specified := true
-let set_rcuser s = rcfile := Filename.concat ("~"^s) ".coqrc"
+let set_rcuser s = rcfile := ("~"^s)/".coqrc"
 
 let load_rc = ref true
 let no_load_rc () = load_rc := false
@@ -77,7 +79,7 @@ let init_load_path () =
       (* variable COQLIB overrides the default library *)
     else getenv_else "COQLIB" Coq_config.coqlib in
   (* first user-contrib *)
-  let user_contrib = Filename.concat coqlib "user-contrib" in
+  let user_contrib = coqlib/"user-contrib" in
   if Sys.file_exists user_contrib then 
     Mltop.add_path user_contrib Nameops.default_root_prefix;
   (* then standard library *)
@@ -85,8 +87,8 @@ let init_load_path () =
     if !Options.v7 then [ "theories7"; "contrib7" ]
     else [ "theories"; "contrib" ] in
   let dirs = 
-    (if !Options.v7 then "states7" else "states") :: dev @ vdirs @ [ "ide" ] in
-  List.iter (fun s -> coq_add_rec_path (Filename.concat coqlib s)) dirs;
+    (if !Options.v7 then "states7" else "states") :: dev @ vdirs in
+  List.iter (fun s -> coq_add_rec_path (coqlib/s)) dirs;
   let camlp4 = getenv_else "CAMLP4LIB" Coq_config.camlp4lib in
   add_ml_include camlp4;
   (* then current directory *)
@@ -101,13 +103,13 @@ let init_library_roots () =
 
 (* Initialises the Ocaml toplevel before launching it, so that it can
    find the "include" file in the *source* directory *)
-let init_ocaml_path () =
 (* We only assume that the variable COQTOP is set *)
+let init_ocaml_path () =
   let coqtop = getenv_else "COQTOP" Coq_config.coqtop in
   let add_subdir dl = 
-    Mltop.add_ml_dir (List.fold_left Filename.concat coqtop dl) 
+    Mltop.add_ml_dir (List.fold_left (/) coqtop dl) 
   in
   List.iter add_subdir
     [ [ "config" ]; [ "dev" ]; [ "lib" ]; [ "kernel" ]; [ "library" ]; 
       [ "pretyping" ]; [ "interp" ]; [ "parsing" ]; [ "proofs" ];
-      [ "tactics" ]; [ "toplevel" ] ]
+      [ "tactics" ]; [ "toplevel" ]; [ "translate" ]; [ "ide" ] ]
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 72ac4f086a..9561d03252 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -137,7 +137,7 @@ let re_exec () =
       if dir <> "." then Filename.concat dir com else com 
     in
     Sys.argv.(0) <- newprog;
-    Unix.handle_unix_error Unix.execvp newprog Sys.argv
+    Unix.handle_unix_error (Unix.execvp newprog) Sys.argv
   end
 
 (*s Parsing of the command line.
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 2b7688f8d3..ade7f0e940 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -46,7 +46,6 @@ let pr_db ctx i =
   with Not_found -> str"UNBOUND_REL_"++int i
 
 let explain_unbound_rel ctx n =
-  let ctx = make_all_name_different ctx in
   let pe = pr_ne_context_of (str "In environment") ctx in
   str"Unbound reference: " ++ pe ++
   str"The reference " ++ int n ++ str " is free"
@@ -56,7 +55,6 @@ let explain_unbound_var ctx v =
   str"No such section variable or assumption : " ++ var
 
 let explain_not_type ctx j =
-  let ctx = make_all_name_different ctx in
   let pe = pr_ne_context_of (str"In environment") ctx in
   let pc,pt = prjudge_env ctx j in
   pe ++ str "the term" ++ brk(1,1) ++ pc ++ spc () ++
@@ -64,7 +62,6 @@ let explain_not_type ctx j =
   str"which should be Set, Prop or Type."
 
 let explain_bad_assumption ctx j =
-  let ctx = make_all_name_different ctx in
   let pe = pr_ne_context_of (str"In environment") ctx in
   let pc,pt = prjudge_env ctx j in
   pe ++ str "cannot declare a variable or hypothesis over the term" ++
@@ -140,7 +137,6 @@ let explain_ill_formed_branch ctx c i actty expty =
   str "which should be" ++ brk(1,1) ++ pe
 
 let explain_generalization ctx (name,var) j =
-  let ctx = make_all_name_different ctx in
   let pe = pr_ne_context_of (str "In environment") ctx in
   let pv = prtype_env ctx var in
   let (pc,pt) = prjudge_env (push_rel_assum (name,var) ctx) j in
@@ -151,7 +147,6 @@ let explain_generalization ctx (name,var) j =
   spc () ++ str"which should be Set, Prop or Type."
 
 let explain_actual_type ctx j pt =
-  let ctx = make_all_name_different ctx in
   let pe = pr_ne_context_of (str "In environment") ctx in
   let (pc,pct) = prjudge_env ctx j in
   let pt = prterm_env ctx pt in
@@ -161,7 +156,6 @@ let explain_actual_type ctx j pt =
   str "while it is expected to have type" ++ brk(1,1) ++ pt
 
 let explain_cant_apply_bad_type ctx (n,exptyp,actualtyp) rator randl =
-  let ctx = make_all_name_different ctx in
   let randl = Array.to_list randl in
 (*  let pe = pr_ne_context_of (str"in environment") ctx in*)
   let pr,prt = prjudge_env ctx rator in
@@ -184,7 +178,6 @@ let explain_cant_apply_bad_type ctx (n,exptyp,actualtyp) rator randl =
   str"which should be coercible to" ++ brk(1,1) ++ prterm_env ctx exptyp
 
 let explain_cant_apply_not_functional ctx rator randl =
-  let ctx = make_all_name_different ctx in
   let randl = Array.to_list randl in
 (*  let pe = pr_ne_context_of (str"in environment") ctx in*)
   let pr = prterm_env ctx rator.uj_val in
@@ -204,7 +197,6 @@ let explain_cant_apply_not_functional ctx rator randl =
   str" " ++ v 0 appl
 
 let explain_unexpected_type ctx actual_type expected_type =
-  let ctx = make_all_name_different ctx in
   let pract = prterm_env ctx actual_type in
   let prexp = prterm_env ctx expected_type in
   str"This type is" ++ spc () ++ pract ++ spc () ++ 
@@ -212,7 +204,6 @@ let explain_unexpected_type ctx actual_type expected_type =
   spc () ++ prexp
 
 let explain_not_product ctx c =
-  let ctx = make_all_name_different ctx in
   let pr = prterm_env ctx c in
   str"The type of this term is a product," ++ spc () ++
   str"but it is casted with type" ++
@@ -304,13 +295,13 @@ let explain_ill_typed_rec_body ctx i names vdefj vargs =
   str"recursive definition"  ++ spc () ++ pvd ++ spc () ++
   str "has type" ++ spc () ++ pvdt ++spc () ++ 
   str "it should be" ++ spc () ++ pv 
-
+(*
 let explain_not_inductive ctx c =
   let ctx = make_all_name_different ctx in
   let pc = prterm_env ctx c in
   str"The term" ++ brk(1,1) ++ pc ++ spc () ++
   str "is not an inductive definition"
-
+*)
 let explain_cant_find_case_type ctx c =
   let ctx = make_all_name_different ctx in
   let pe = prterm_env ctx c in
@@ -375,7 +366,9 @@ let explain_wrong_case_info ctx ind ci =
     spc () ++ pc
        
 
-let explain_type_error ctx = function
+let explain_type_error ctx err =
+  let ctx = make_all_name_different ctx in
+  match err with
   | UnboundRel n -> 
       explain_unbound_rel ctx n
   | UnboundVar v -> 
@@ -412,7 +405,9 @@ let explain_type_error ctx = function
   | NotInductive c ->
       explain_not_inductive ctx c
 *)
-let explain_pretype_error ctx = function
+let explain_pretype_error ctx err =
+  let ctx = make_all_name_different ctx in
+  match err with
   | CantFindCaseType c ->
       explain_cant_find_case_type ctx c
   | OccurCheck (n,c) ->
diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml
index cbf9de04f5..602fcf171e 100644
--- a/toplevel/toplevel.ml
+++ b/toplevel/toplevel.ml
@@ -317,7 +317,7 @@ let rec coq_switch b =
     | End_of_input -> msgerrnl (mt ()); pp_flush(); exit 0
     | Vernacexpr.Quit -> exit 0
     | e ->
-	msgerrnl (str"Anomaly: toplevel loop. Please report.");
+	msgerrnl (str"Anomaly. Please report.");
 	coq_switch b
 
 let loop () = coq_switch true