amelioration des messages d'erreurs vis a vis des evars

ajout automatique des chemins vers les sources au moment du Drop


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

7 files changed, 87 insertions, 65 deletions

diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index 01dec915a0..80c81d243b 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -91,3 +91,16 @@ let init_library_roots () =
   List.iter
     (fun (_,alias,_) -> Nametab.push_library_root (List.hd alias)) !includes;
   includes := []
+
+(* 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 coqtop = getenv_else "COQTOP" Coq_config.coqtop in
+  let add_subdir dl = 
+    Mltop.add_ml_dir (List.fold_left Filename.concat coqtop dl) 
+  in
+  List.iter add_subdir
+    [ [ "config" ]; [ "dev" ]; [ "lib" ]; [ "kernel" ]; [ "library" ]; 
+      [ "pretyping" ]; [ "parsing" ]; [ "proofs" ]; [ "tactics" ];
+      [ "toplevel" ] ]
diff --git a/toplevel/coqinit.mli b/toplevel/coqinit.mli
index 81a83eeead..af2c27be9e 100644
--- a/toplevel/coqinit.mli
+++ b/toplevel/coqinit.mli
@@ -23,3 +23,5 @@ val push_rec_include : string * Names.dir_path -> unit
 
 val init_load_path : unit -> unit
 val init_library_roots : unit -> unit
+
+val init_ocaml_path : unit -> unit
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 27bb17d850..befe4cf43b 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -213,6 +213,10 @@ let start () =
       exit 1
   end;
   if !batch_mode then (flush_all(); Profile.print_profile ();exit 0);
-  Toplevel.loop()
+  Toplevel.loop();
+(* Initialise and launch the Ocaml toplevel *)
+  Coqinit.init_ocaml_path();
+  Mltop.ocaml_toploop();
+  exit 1
 
 (* [Coqtop.start] will be called by the code produced by coqmktop *)
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 4daec6d523..e9194d8a85 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -63,12 +63,12 @@ let msg_bad_elimination ctx k = function
   | None -> 
       [<>]
 
-let explain_elim_arity k ctx ind aritylst c p pt okinds = 
+let explain_elim_arity k ctx ind aritylst c pj okinds = 
   let pi = pr_inductive ctx ind in
   let ppar = prlist_with_sep pr_coma (prterm_env ctx) aritylst in
   let pc = prterm_env ctx c in
-  let pp = prterm_env ctx p in
-  let ppt = prterm_env ctx pt in
+  let pp = prterm_env ctx pj.uj_val in
+  let ppt = prterm_env ctx pj.uj_type in
   [< 'sTR "Incorrect elimination of"; 'bRK(1,1); pc; 'sPC;
      'sTR "in the inductive type"; 'bRK(1,1); pi; 'fNL;
      'sTR "The elimination predicate"; 'bRK(1,1); pp; 'sPC;
@@ -76,16 +76,16 @@ let explain_elim_arity k ctx ind aritylst c p pt okinds =
      'sTR "It should be one of :"; 'bRK(1,1) ; hOV 0 ppar; 'fNL;
      msg_bad_elimination ctx k okinds >]
 
-let explain_case_not_inductive k ctx c ct =
-  let pc = prterm_env ctx c in
-  let pct = prterm_env ctx ct in
+let explain_case_not_inductive k ctx cj =
+  let pc = prterm_env ctx cj.uj_val in
+  let pct = prterm_env ctx cj.uj_type in
   [< 'sTR "In Cases expression, the matched term"; 'bRK(1,1); pc; 'sPC; 
      'sTR "has type"; 'bRK(1,1); pct; 'sPC; 
      'sTR "which is not a (co-)inductive type" >]
   
-let explain_number_branches k ctx c ct expn =
-  let pc = prterm_env ctx c in
-  let pct = prterm_env ctx ct in
+let explain_number_branches k ctx cj expn =
+  let pc = prterm_env ctx cj.uj_val in
+  let pct = prterm_env ctx cj.uj_type in
   [< 'sTR "Cases on term"; 'bRK(1,1); pc; 'sPC ;
      'sTR "of type"; 'bRK(1,1); pct; 'sPC;
      'sTR "expects ";  'iNT expn; 'sTR " branches" >]
@@ -159,20 +159,21 @@ let explain_cant_apply_not_functional k ctx rator randl =
      'sTR"The expression"; 'bRK(1,1); pr; 'sPC;
      'sTR"of type"; 'bRK(1,1); prt; 'sPC ;
      'sTR("cannot be applied to the "^term_string); 'fNL; 
-     'sTR" "; v 0 appl; 'fNL >]
+     'sTR" "; v 0 appl >]
 
 let explain_unexpected_type k 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; 'sTR "but is expected to be";
-     'sPC; prexp; 'fNL >]
+     'sPC; prexp >]
 
 let explain_not_product k ctx c =
   let ctx = make_all_name_different ctx in
   let pr = prterm_env ctx c in
-  [< 'sTR"The type of this term is expected to be a product but it is";
-     'bRK(1,1); pr; 'fNL >]
+  [< 'sTR"The type of this term is a product,"; 'sPC;
+     'sTR"but it is casted with type";
+     'bRK(1,1); pr >]
 
 (* TODO: use the names *)
 (* (co)fixpoints *)
@@ -248,15 +249,6 @@ let explain_cant_find_case_type k ctx c =
   let pe = prterm_env ctx c in
   hOV 3 [<'sTR "Cannot infer type of whole Case expression on"; 'wS 1; pe >]
 
-(***
-let explain_cant_find_case_type_loc loc k ctx c =
-  let pe = prterm_env ctx c in
-  user_err_loc
-    (loc,"pretype",
-     hOV 3 [<'sTR "Cannot infer type of whole Case expression on"; 
-	     'wS 1; pe >])
-***)
-
 let explain_occur_check k ctx ev rhs =
   let id = "?" ^ string_of_int ev in
   let pt = prterm_env ctx rhs in
@@ -285,12 +277,12 @@ let explain_type_error k ctx = function
       explain_bad_assumption k ctx c
   | ReferenceVariables id -> 
       explain_reference_variables id
-  | ElimArity (ind, aritylst, c, p, pt, okinds) ->
-      explain_elim_arity k ctx ind aritylst c p pt okinds 
-  | CaseNotInductive (c, ct) -> 
-      explain_case_not_inductive k ctx c ct
-  | NumberBranches (c, ct, n) -> 
-      explain_number_branches k ctx c ct n
+  | ElimArity (ind, aritylst, c, pj, okinds) ->
+      explain_elim_arity k ctx ind aritylst c pj okinds 
+  | CaseNotInductive cj -> 
+      explain_case_not_inductive k ctx cj
+  | NumberBranches (cj, n) -> 
+      explain_number_branches k ctx cj n
   | IllFormedBranch (c, i, actty, expty) -> 
       explain_ill_formed_branch k ctx c i actty expty 
   | Generalization (nvar, c) ->
@@ -310,7 +302,7 @@ let explain_type_error k ctx = function
       explain_not_inductive k ctx c
 *)
 let explain_pretype_error ctx = function
-  | MlCase mes ->
+  | MlCase (mes,_,_) ->
       explain_ml_case CCI ctx mes
   | CantFindCaseType c ->
       explain_cant_find_case_type CCI ctx c
diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4
index 531e527522..0499eff838 100644
--- a/toplevel/mltop.ml4
+++ b/toplevel/mltop.ml4
@@ -51,7 +51,8 @@ let keep_copy_mlpath s =
 type toplevel = { 
   load_obj : string -> unit;
   use_file : string -> unit;
-  add_dir  : string -> unit }
+  add_dir  : string -> unit;
+  ml_loop  : unit -> unit }
 
 (* Determines the behaviour of Coq with respect to ML files (compiled 
    or not) *)
@@ -82,6 +83,16 @@ let enable_load () =
     | WithTop _ | WithoutTop -> true
     |_ -> false
 
+(* Runs the toplevel loop of Ocaml *)
+let ocaml_toploop () =
+  match !load with
+    | WithTop t -> Printexc.catch t.ml_loop ()
+    | _ -> ()
+(*
+        errorlabstrm "Mltop.ocaml_toploop"
+          [< 'sTR"Cannot access the ML toplevel" >]
+*)
+
 (* Dynamic loading of .cmo *)
 let dir_ml_load s = 
   match !load with
diff --git a/toplevel/mltop.mli b/toplevel/mltop.mli
index 17c3f192f2..8e493ad02e 100644
--- a/toplevel/mltop.mli
+++ b/toplevel/mltop.mli
@@ -10,10 +10,11 @@
 
 (* If there is a toplevel under Coq, it is described by the following 
    record. *)
-type toplevel = {
+type toplevel = { 
   load_obj : string -> unit;
   use_file : string -> unit;
-  add_dir : string -> unit }
+  add_dir  : string -> unit;
+  ml_loop  : unit -> unit }
 
 (* Determines the behaviour of Coq with respect to ML files (compiled 
    or not) *) 
@@ -35,6 +36,9 @@ val is_ocaml_top : unit -> bool
 (*Tests if we can load ML files*)
 val enable_load : unit -> bool
 
+(*Starts the Ocaml toplevel loop *)
+val ocaml_toploop : unit -> unit
+
 (*Dynamic loading of .cmo*)
 val dir_ml_load : string -> unit
 
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index fbc9dc1522..8d684633b8 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -14,22 +14,16 @@ open Declarations
 open Pp
 open Util
 open Options
-open Stamps
 open System
 open Names
 open Term
-open Evd
-open Reduction
 open Pfedit
 open Tacmach
 open Proof_trees
 open Proof_type
 open Tacred
-open Library
-open Libobject
 open Environ
 open Vernacinterp
-open Declare
 open Coqast
 open Ast
 open Astterm
@@ -39,8 +33,7 @@ open Tacinterp
 open Tactic_debug
 open Command
 open Goptions
-open Mltop
-open Nametab
+open Declare
 
 (* Dans join_binders, s'il y a un "?", on perd l'info qu'il est partagé *)
 let join_binders binders = 
@@ -121,7 +114,7 @@ let locate_qualid loc qid =
     let _ = Syntax_def.locate_syntactic_definition qid in
     error
       ("Unexpected reference to a syntactic definition: "
-       ^(string_of_qualid qid))
+       ^(Nametab.string_of_qualid qid))
   with Not_found ->
     Nametab.error_global_not_found_loc loc qid
 
@@ -130,7 +123,8 @@ let global = locate_qualid
 
 let locate_file f =
   try
-    let _,file = System.where_in_path (get_load_path()) f in
+    let _,file =
+      System.where_in_path (Library.get_load_path()) f in
     mSG [< 'sTR file; 'fNL >]
   with Not_found -> 
     mSG (hOV 0 [< 'sTR"Can't find file"; 'sPC; 'sTR f; 'sPC;
@@ -147,13 +141,13 @@ let print_located_qualid qid =
       [< 'sTR (string_of_path (Syntax_def.locate_syntactic_definition qid));
 	 'fNL >]
   with Not_found ->
-    error ((string_of_qualid qid) ^ " not a defined object")
+    error ((Nametab.string_of_qualid qid) ^ " not a defined object")
 
 let print_path_entry s =
   [< 'sTR s.directory; 'tBRK (0,2); 'sTR (string_of_dirpath s.coq_dirpath) >]
 
 let print_loadpath () =
-  let l = get_load_path () in
+  let l = Library.get_load_path () in
   mSGNL (Pp.t [< 'sTR "Physical path:                                 ";
 		 'tAB; 'sTR "Logical Path:"; 'fNL; 
 		 prlist_with_sep pr_fnl print_path_entry l >])
@@ -193,29 +187,29 @@ let _ =
   add "ADDPATH"
     (function 
        | [VARG_STRING dir] ->
-	   (fun () -> add_path dir [Nametab.default_root])
+	   (fun () -> Mltop.add_path dir [Nametab.default_root])
        | [VARG_STRING dir ; VARG_QUALID alias] ->
            let aliasdir,aliasname = Nametab.repr_qualid alias in
-	    (fun () -> add_path dir (aliasdir@[string_of_id aliasname]))
+	    (fun () -> Mltop.add_path dir (aliasdir@[string_of_id aliasname]))
        | _ -> bad_vernac_args "ADDPATH")
 
 (* For compatibility *)
 let _ =
   add "DELPATH"
     (function 
-       | [VARG_STRING dir] -> (fun () -> remove_path dir)
+       | [VARG_STRING dir] -> (fun () -> Library.remove_path dir)
        | _ -> bad_vernac_args "DELPATH")
 
 let _ = 
   add "RECADDPATH"
     (function 
        | [VARG_STRING dir] ->
-	   (fun () -> add_rec_path dir [Nametab.default_root])
+	   (fun () -> Mltop.add_rec_path dir [Nametab.default_root])
        | [VARG_STRING dir ; VARG_QUALID alias] ->
            let aliasdir,aliasname = Nametab.repr_qualid alias in
 	    (fun () ->
 	       let alias = aliasdir@[string_of_id aliasname] in
-	       add_rec_path dir alias;
+	       Mltop.add_rec_path dir alias;
 	       Nametab.push_library_root (List.hd alias))
        | _ -> bad_vernac_args "RECADDPATH")
 
@@ -395,7 +389,7 @@ let _ =
        | [VARG_CONSTR com] ->
 	   (fun () ->
               if not (refining()) then begin
-              	start_proof_com None NeverDischarge com;
+              	start_proof_com None Declare.NeverDischarge com;
 		if_verbose show_open_subgoals ()
               end else 
 		error "repeated Goal not permitted in refining mode")
@@ -553,11 +547,11 @@ let _ =
 		   let coe = coercion_of_qualid dummy_loc qid in
 	           if Classops.is_coercion_visible coe then
 		     message
-		       ("Printing of coercion "^(string_of_qualid qid)^
+		       ("Printing of coercion "^(Nametab.string_of_qualid qid)^
 			" is set")
 		   else 
 		     message 
-		       ("Printing of coercion "^(string_of_qualid qid)^
+		       ("Printing of coercion "^(Nametab.string_of_qualid qid)^
 			" is unset"))
 		ql))
     
@@ -714,7 +708,7 @@ let _ =
 			 (fun (mv,ty) -> 
 			    [< 'iNT mv ; 'sTR" -> " ; prtype ty ; 'fNL >])
 			 meta_types;
-		       'sTR"Proof: " ; prterm (nf_ise1 evc pfterm) >])
+		       'sTR"Proof: " ; prterm (Evarutil.nf_evar evc pfterm) >])
        | _ -> bad_vernac_args "ShowProof")
 
 let _ =
@@ -1026,7 +1020,7 @@ let extract_qualid = function
   | VARG_QUALID qid ->
       (try wd_of_sp (fst (Nametab.locate_module qid))
        with Not_found -> 
-	 error ("Module/section "^(string_of_qualid qid)^" not found"))
+	 error ("Module/section "^(Nametab.string_of_qualid qid)^" not found"))
   | _ -> bad_vernac_args "extract_qualid"
 
 let inside_outside = function
@@ -1349,11 +1343,12 @@ let _ =
 	   fun () -> 
 	     let ref = locate_qualid dummy_loc qid in
 	     Class.try_add_new_class ref stre;
-             if_verbose message ((string_of_qualid qid) ^ " is now a class")
+             if_verbose message
+               ((Nametab.string_of_qualid qid) ^ " is now a class")
        | _ -> bad_vernac_args "CLASS")
 
 let cl_of_qualid qid =
-  match repr_qualid qid with
+  match Nametab.repr_qualid qid with
     | [], id when string_of_id id = "FUNCLASS" -> Classops.CL_FUN
     | [], id when string_of_id id = "SORTCLASS" -> Classops.CL_SORT
     | _ -> Class.class_of_ref (locate_qualid dummy_loc qid)	
@@ -1373,7 +1368,7 @@ let _ =
 	   let target = cl_of_qualid qidt in
 	   let source = cl_of_qualid qids in
 	   fun () ->
-	     if isid then match repr_qualid qid with
+	     if isid then match Nametab.repr_qualid qid with
 	       | [], id ->
 		   Class.try_add_new_identity_coercion id stre source target
 	       | _ -> bad_vernac_args "COERCION"
@@ -1381,7 +1376,8 @@ let _ =
 	       let ref = locate_qualid dummy_loc qid in
 	       Class.try_add_new_coercion_with_target ref stre source target;
 	       if_verbose
-		 message ((string_of_qualid qid) ^ " is now a coercion")
+		 message
+                 ((Nametab.string_of_qualid qid) ^ " is now a coercion")
        | _ -> bad_vernac_args "COERCION")
 
 let _ =
@@ -1672,7 +1668,7 @@ let _ =
             if (string_of_id t) = "Tables" then 
 	      print_tables ()
 	    else 
-	      mSG(print_name (make_qualid [] t)))
+	      mSG(print_name (Nametab.make_qualid [] t)))
      | _ -> bad_vernac_args "TableField")
 
 
@@ -1736,26 +1732,26 @@ let _ = vinterp_add "DeclareMLModule"
 		    | (VARG_STRING s) -> s 
 		    | _ -> anomaly "DeclareMLModule : not a string") l
 	     in
-    	     fun () -> declare_ml_modules sl)
+    	     fun () -> Mltop.declare_ml_modules sl)
 	  
 let _ = vinterp_add "AddMLPath"
 	  (function 
 	     | [VARG_STRING s] ->
-		 (fun () -> add_ml_dir (glob s))
+		 (fun () -> Mltop.add_ml_dir (glob s))
 	     | _ -> anomaly "AddMLPath : not a string")
 
 let _ = vinterp_add "RecAddMLPath"
 	  (function 
 	     | [VARG_STRING s] ->
-		 (fun () -> add_rec_ml_dir (glob s))
+		 (fun () -> Mltop.add_rec_ml_dir (glob s))
 	     | _ -> anomaly "RecAddMLPath : not a string")
 
 let _ = vinterp_add "PrintMLPath"
 	  (function 
-	     | [] -> (fun () -> print_ml_path ())
+	     | [] -> (fun () -> Mltop.print_ml_path ())
 	     | _ -> anomaly "PrintMLPath : does not expect any argument")
 
 let _ = vinterp_add "PrintMLModules"
 	  (function 
-	     | [] -> (fun () -> print_ml_modules ())
+	     | [] -> (fun () -> Mltop.print_ml_modules ())
 	     | _ -> anomaly "PrintMLModules : does not expect an argument")