- états fabriqués avec -silent

 - compilation theories avec -q
 - correction but de tclORELSE qui doit maintenant rattraper aussi
   TypeError et RefinerError


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

5 files changed, 48 insertions, 16 deletions

diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index 33ee012cf0..5253f9fb7e 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -30,12 +30,15 @@ let load_rcfile() =
         Vernac.load_vernac false (!rcfile^"."^Coq_config.version)
       else if file_readable_p !rcfile then
         Vernac.load_vernac false !rcfile
-      else mSGNL [< 'sTR ("No .coqrc or .coqrc."^Coq_config.version^
-		   " found. Skipping rcfile loading.") >]
+      else 
+	if Options.is_verbose() then 
+	  mSGNL [< 'sTR ("No .coqrc or .coqrc."^Coq_config.version^
+			 " found. Skipping rcfile loading.") >]
     with e ->
       (mSGNL [< 'sTR"Load of rcfile failed." >];
        raise e)
-  else mSGNL [< 'sTR"Skipping rcfile loading." >]
+  else 
+    if Options.is_verbose() then mSGNL [< 'sTR"Skipping rcfile loading." >]
 
 (* Puts dir in the path of ML and in the LoadPath *)
 let add_include s =
diff --git a/toplevel/errors.ml b/toplevel/errors.ml
index ba1f36cd7c..ad4f6f389b 100644
--- a/toplevel/errors.ml
+++ b/toplevel/errors.ml
@@ -52,6 +52,8 @@ let rec explain_exn_default = function
 
   | InductiveError e -> hOV 0 (Himsg.explain_inductive_error e)
 
+  | Logic.RefinerError e -> hOV 0 (Himsg.explain_refiner_error e)
+
   | Stdpp.Exc_located (loc,exc) ->
       hOV 0 [< if loc = Ast.dummy_loc then [<>]
                else [< 'sTR"At location "; print_loc loc; 'sTR":"; 'fNL >];
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index ff96d59a6d..a7cc960abd 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -12,6 +12,7 @@ open Sign
 open Environ
 open Type_errors
 open Reduction
+open Logic
 open Pretty
 open Printer
 open Ast
@@ -285,24 +286,47 @@ let explain_type_error k ctx = function
   | NeedsInversion (x,t) ->
       explain_needs_inversion k ctx x t
 
-let explain_refiner_bad_type k ctx arg ty conclty =
+let explain_refiner_bad_type arg ty conclty =
   [< 'sTR"refiner was given an argument"; 'bRK(1,1); 
-     gentermpr k ctx arg; 'sPC;
-     'sTR"of type"; 'bRK(1,1); gentermpr k ctx ty; 'sPC;
-     'sTR"instead of"; 'bRK(1,1); gentermpr k ctx conclty >]
+     prterm arg; 'sPC;
+     'sTR"of type"; 'bRK(1,1); prterm ty; 'sPC;
+     'sTR"instead of"; 'bRK(1,1); prterm conclty >]
 
-let explain_refiner_occur_meta k ctx t =
-  [< 'sTR"cannot refine with term"; 'bRK(1,1); gentermpr k ctx t;
+let explain_refiner_occur_meta t =
+  [< 'sTR"cannot refine with term"; 'bRK(1,1); prterm t;
      'sPC; 'sTR"because there are metavariables, and it is";
      'sPC; 'sTR"neither an application nor a Case" >]
 
-let explain_refiner_cannot_applt k ctx t harg =
+let explain_refiner_cannot_applt t harg =
   [< 'sTR"in refiner, a term of type "; 'bRK(1,1);
-     gentermpr k ctx t; 'sPC; 'sTR"could not be applied to"; 'bRK(1,1);
-     gentermpr k ctx harg >]
-
-let explain_refiner_error e =
-  [< 'sTR "TODO: EXPLAIN REFINER ERROR" >]
+     prterm t; 'sPC; 'sTR"could not be applied to"; 'bRK(1,1);
+     prterm harg >]
+
+let explain_refiner_cannot_unify m n =
+  let pm = prterm m in 
+  let pn = prterm n in
+  [< 'sTR"Impossible to unify"; 'bRK(1,1) ; pm; 'sPC ;
+     'sTR"with"; 'bRK(1,1) ; pn >]
+
+let explain_refiner_cannot_generalize ty =
+  [< 'sTR "cannot find a generalisation of the goal with type : "; 
+     prterm ty >]
+
+let explain_refiner_not_well_typed c =
+  [< 'sTR"The term " ; prterm c ; 'sTR" is not well-typed" >]
+
+let explain_refiner_bad_tactic_args s l =
+  [< 'sTR "Internal tactic "; 'sTR s; 'sTR " cannot be applied to ";
+     Tacmach.pr_tactic (s,l) >]
+
+let explain_refiner_error = function
+  | BadType (arg,ty,conclty) -> explain_refiner_bad_type arg ty conclty
+  | OccurMeta t -> explain_refiner_occur_meta t
+  | CannotApply (t,harg) -> explain_refiner_cannot_applt t harg
+  | CannotUnify (m,n) -> explain_refiner_cannot_unify m n
+  | CannotGeneralize (_,ty) -> explain_refiner_cannot_generalize ty
+  | NotWellTyped c -> explain_refiner_not_well_typed c
+  | BadTacticArgs (s,l) -> explain_refiner_bad_tactic_args s l
 
 let error_non_strictly_positive k lna c v  =
   let env = assumptions_for_print lna in
diff --git a/toplevel/himsg.mli b/toplevel/himsg.mli
index d12d7963e5..7bf0ef9c8d 100644
--- a/toplevel/himsg.mli
+++ b/toplevel/himsg.mli
@@ -7,6 +7,7 @@ open Names
 open Inductive
 open Sign
 open Type_errors
+open Logic
 (*i*)
 
 (* This module provides functions to explain the type errors. *)
@@ -14,3 +15,5 @@ open Type_errors
 val explain_type_error : path_kind -> context -> type_error -> std_ppcmds
 
 val explain_inductive_error : inductive_error -> std_ppcmds
+
+val explain_refiner_error : refiner_error -> std_ppcmds
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index e53dea4ded..9781eb2e7d 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -72,7 +72,7 @@ let add_token_obj s = Lib.add_anonymous_leaf (inToken s)
 let (inGrammar, outGrammar) =
   declare_object
     ("GRAMMAR",
-     { load_function = (fun _ -> ());
+     { load_function = (fun (_, a) -> Egrammar.extend_grammar a);
        open_function = (fun _ -> ());
        cache_function = (fun (_, a) -> Egrammar.extend_grammar a);
        specification_function = (fun x -> x)})