quelques bug reports mineurs

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

3 files changed, 9 insertions, 5 deletions

diff --git a/lib/system.mli b/lib/system.mli
index 5c893eb30e..ee2dca4905 100644
--- a/lib/system.mli
+++ b/lib/system.mli
@@ -49,8 +49,6 @@ val raw_extern_intern : int -> string ->
 val extern_intern : 
   int -> string -> (string -> 'a -> unit) * (load_path -> string -> 'a)
 
-val open_trapping_failure : (string -> 'a) -> string -> string -> 'a
-
 (*s Time stamps. *)
 
 type time
diff --git a/library/library.ml b/library/library.ml
index b30852e7d0..48af3672af 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -144,7 +144,13 @@ let rec load_module_from s f =
   try
     Stringmap.find s !modules_table
   with Not_found ->
-    let (lpe,fname,ch) = raw_intern_module (get_load_path ()) f in
+    let (lpe,fname,ch) =
+      try raw_intern_module (get_load_path ()) f
+      with System.Bad_magic_number fname ->
+        errorlabstrm "load_module_from"
+          [< 'sTR"file "; 'sTR fname; 'sPC; 'sTR"has bad magic number.";
+             'sPC; 'sTR"It is corrupted"; 'sPC;
+             'sTR"or was compiled with another version of Coq." >] in
     let md = System.marshal_in ch in
     let digest = System.marshal_in ch in
     close_in ch;
diff --git a/proofs/tacinterp.ml b/proofs/tacinterp.ml
index c6c8cfe6cd..6730419a99 100644
--- a/proofs/tacinterp.ml
+++ b/proofs/tacinterp.ml
@@ -579,8 +579,8 @@ and app_interp (evc,env,lfun,lmatch,goalopt,debug) fv largs ast =
       else
         VFun(olfun@newlfun,lvar,body)
     | _ ->
-      anomaly_loc (Ast.loc ast, "Tacinterp.app_interp",[<'sTR
-        "Illegal application: "; print_ast ast>])
+      user_err_loc (Ast.loc ast, "Tacinterp.app_interp",[<'sTR
+        "Illegal tactic application: "; print_ast ast>])
 
 (* Interprets recursive expressions *)
 and rec_interp (evc,env,lfun,lmatch,goalopt,debug) ast = function