- méthode load sur les Hints

 - CAST pris en compte dans Astterm
 - Coercin.lookup_path_to_sort_from protégé par un try/with


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

9 files changed, 40 insertions, 32 deletions

diff --git a/library/goptions.ml b/library/goptions.ml
index a8b553f328..3a697cb6d3 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -213,8 +213,8 @@ let declare_async_option cast uncast
     let _ = get_option key in
     error "Sorry, this option name is already used"
   with Not_found ->
-    if List.mem_assoc (nickname key) !param_table
-    then error "Sorry, this option name is already used";
+    if List.mem_assoc (nickname key) !param_table then 
+      error "Sorry, this option name is already used";
     let cread () = cast (read ()) in
     let cwrite v = write (uncast v) in
     async_value_tab := OptionMap.add key (name,(cread,cwrite)) !async_value_tab
diff --git a/parsing/astterm.ml b/parsing/astterm.ml
index 68cd5482d9..7dad63a008 100644
--- a/parsing/astterm.ml
+++ b/parsing/astterm.ml
@@ -315,6 +315,9 @@ let dbize k sigma =
     | Node(loc,("CONST"|"EVAR"|"MUTIND"|"MUTCONSTRUCT"|"SYNCONST" as key),l) ->
 	dbize_global loc (key,l)
 
+    | Node(loc,"CAST", [c1;c2]) ->	   
+	RCast (loc,dbrec env c1,dbrec env c2)
+
     | Node(loc,opn,tl) -> 
 	anomaly ("dbize found operator "^opn^" with "^
 		 (string_of_int (List.length tl))^" arguments")
diff --git a/parsing/lexer.mll b/parsing/lexer.mll
index 410bcc4fa6..e9b57a1f75 100644
--- a/parsing/lexer.mll
+++ b/parsing/lexer.mll
@@ -120,7 +120,7 @@ let identchar =
   ['$' 'A'-'Z' 'a'-'z' '_' '\192'-'\214' '\216'-'\246' '\248'-'\255' 
    '\'' '0'-'9']
 let symbolchar =
-  ['!' '$' '%' '&' '*' '+' '-' '<' '>' '/' ':' ',' ';' '=' '?' '@' '^'
+  ['!' '$' '%' '&' '*' '+' '-' '<' '>' '/' '\\' ':' ',' ';' '=' '?' '@' '^'
    '|' '~' '#']
 let decimal_literal = ['0'-'9']+
 let hex_literal = '0' ['x' 'X'] ['0'-'9' 'A'-'F' 'a'-'f']+
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 90884f3826..34cf69ac2a 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -76,8 +76,11 @@ let inh_app_fun env isevars j =
 
 let inh_tosort_force env isevars j =
   let t,i1 = class_of1 env !isevars j.uj_type in
-  let p = lookup_path_to_sort_from i1 in
-  apply_pcoercion env p j t 
+  try
+    let p = lookup_path_to_sort_from i1 in
+    apply_pcoercion env p j t 
+  with Not_found -> 
+    j
 
 let inh_tosort env isevars j = 
   let typ = whd_betadeltaiota env !isevars j.uj_type in
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index ab2a0c5135..4b3b797bf8 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -178,7 +178,7 @@ let save_named opacity =
     ({ const_entry_body = Cooked pfterm; const_entry_type = Some concl }, 
      strength);
   del_proof ident;
-  message(ident ^ " is defined")
+  if Options.is_verbose() then message (ident ^ " is defined")
     
 let save_anonymous opacity save_ident n =
   let (pfs,ts) = get_state() 
@@ -197,7 +197,7 @@ let save_anonymous opacity save_ident n =
        strength)
   end;
   del_proof ident;
-  message(save_ident ^ " is defined")
+  if Options.is_verbose() then message (save_ident ^ " is defined")
     
 let save_anonymous_thm opacity id =
   save_anonymous opacity id NeverDischarge
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 6358366b7b..46f2d340a3 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -166,7 +166,7 @@ let specification_autohint x = x
 
 let (inAutoHint,outAutoHint) =
   declare_object ("AUTOHINT",
-                  { load_function = (fun _ -> ());
+                  { load_function = cache_autohint;
                     cache_function = cache_autohint;
 		    open_function = (fun _ -> ());
                     specification_function = specification_autohint })
@@ -203,7 +203,7 @@ let make_apply_entry (eapply,verbose) name (c,cty) =
 	if eapply & (nmiss <> 0) then begin
           if verbose then 
 	    wARN [< 'sTR "the hint: EApply "; prterm c;
-		    'sTR " will only used by EAuto" >]; 
+		    'sTR " will only be used by EAuto" >]; 
           (hdconstr,
            { hname = name;
 	     pri = nb_hyp cty + nmiss;
@@ -234,7 +234,7 @@ let make_resolves name eap (c,cty) =
 (* used to add an hypothesis to the local hint database *)
 let make_resolve_hyp hname htyp = 
   try
-    [make_apply_entry (true, false) hname (mkVar hname, htyp)]
+    [make_apply_entry (true, Options.is_verbose()) hname (mkVar hname, htyp)]
   with 
     | Failure _ -> []
     | UserError _ -> anomaly "Papageno programme comme un blaireau"
@@ -249,7 +249,8 @@ let add_resolves clist dbnames =
 		(List.map (fun (name,c) -> 
 			     let env = Global.env() in
 			     let ty = type_of env Evd.empty c in
-			     make_resolves name (true,true) (c,ty)) clist))
+			     let verbose = Options.is_verbose() in
+			     make_resolves name (true,verbose) (c,ty)) clist))
 	    )))
     dbnames
 
@@ -730,7 +731,8 @@ let rec search_gen decomp n db_list local_db add_sign goal =
 	 let (hid,htyp) = hd_sign (pf_untyped_hyps g') in
 	 let hintl = 
 	   try 
-	     [make_apply_entry (true,false) hid (mkVar hid,htyp)]
+	     [make_apply_entry (true,Options.is_verbose()) 
+		hid (mkVar hid,htyp)]
 	   with Failure _ -> [] 
 	 in
          search_gen decomp n db_list
diff --git a/theories/Init/LogicSyntax.v b/theories/Init/LogicSyntax.v
index aac5a75322..fdcc7624cc 100644
--- a/theories/Init/LogicSyntax.v
+++ b/theories/Init/LogicSyntax.v
@@ -34,15 +34,15 @@ with command8 :=
 
 with command10 :=
   allexplicit [ "ALL" ident($x) ":" command($t) "|" command($p) ]
-                          -> [<<(all $t [$x:$t]$p)>>]
+                          -> [<<(all $t [$x : $t]$p)>>]
 | allimplicit [ "ALL" ident($x) "|" command($p) ]
                           -> [<<(all ? [$x]$p)>>]
 | exexplicit [ "EX" ident($v) ":" command($t) "|" command($c1) ]
-                          -> [<<(ex $t [$v:$t]$c1)>>]
+                          -> [<<(ex $t [$v : $t]$c1)>>]
 | eximplicit [ "EX" ident($v) "|" command($c1) ] 
                           -> [<<(ex ? [$v]$c1)>>]
 | ex2explicit [ "EX" ident($v) ":" command($t) "|" command($c1) "&"
-           command($c2) ] -> [<<(ex2 $t [$v:$t]$c1 [$v:$t]$c2)>>]
+           command($c2) ] -> [<<(ex2 $t [$v : $t]$c1 [$v : t]$c2)>>]
 | ex2implicit [ "EX" ident($v) "|" command($c1) "&" 
            command($c2) ] -> [<<(ex2 ? [$v]$c1 [$v]$c2)>>].
 
@@ -79,14 +79,14 @@ Syntax constr
 
   level 10:
     all_pred [<<(all $_ $p)>>] -> [ [<hov 4> "All " $p:L ] ]
-  | all_imp [<<(all $_ [$x:$T]$t)>>]
+  | all_imp [<<(all $_ [$x : $T]$t)>>]
        -> [ [<hov 3> "ALL " $x ":" $T:L " |" [1 0] $t:L ] ]
 
   | ex_pred [<<(ex $_ $p)>>] -> [ [<hov 0> "Ex " $p:L ] ]
-  | ex [<<(ex $_ [$x:$T]$P)>>] 
+  | ex [<<(ex $_ [$x : $T]$P)>>] 
        -> [ [<hov 2> "EX " $x ":" $T:L " |" [1 0] $P:L ] ]
 
   | ex2_pred [<<(ex2 $_ $p1 $p2)>>]
        -> [ [<hov 3> "Ex2 " $p1:L [1 0] $p2:L ] ]
-  | ex2 [<<(ex2 $_ [$x:$T]$P1 [$x:$T]$P2)>>] 
+  | ex2 [<<(ex2 $_ [$x : T]$P1 [$x : $T]$P2)>>] 
        -> [ [<hov 2> "EX " $x ":" $T:L " |" [1 2] $P1:L [1 0] "& " $P2:L] ].
diff --git a/theories/Init/Peano.v b/theories/Init/Peano.v
index b8bf598afb..4efc6c6934 100755
--- a/theories/Init/Peano.v
+++ b/theories/Init/Peano.v
@@ -29,8 +29,8 @@ Definition pred : nat->nat := [n:nat](Cases n of O => O | (S u) => u end).
 Hint eq_pred : v62 := Resolve (f_equal nat nat pred).
 
 Theorem pred_Sn : (m:nat) m=(pred (S m)).
- Proof.
-Auto.
+Proof.
+  Auto.
 Qed.
 
 Theorem eq_add_S : (n,m:nat) (S n)=(S m) -> n=m.
@@ -44,7 +44,7 @@ Hints Immediate eq_add_S : core v62.
 
 Theorem not_eq_S : (n,m:nat) ~(n=m) -> ~((S n)=(S m)).
 Proof.
- Red; Auto.
+  Red; Auto.
 Qed.
 Hints Resolve not_eq_S : core v62.
 
@@ -62,7 +62,7 @@ Hints Resolve O_S : core v62.
 
 Theorem n_Sn : (n:nat) ~(n=(S n)).
 Proof.
- Induction n ; Auto.
+  Induction n ; Auto.
 Qed.
 Hints Resolve n_Sn : core v62.
 
@@ -79,13 +79,13 @@ Hint eq_nat_binary : core := Resolve (f_equal2 nat nat).
 
 Lemma plus_n_O : (n:nat) n=(plus n O).
 Proof.
- Induction n ; Simpl ; Auto.
+  Induction n ; Simpl ; Auto.
 Qed.
 Hints Resolve plus_n_O : core v62.
 
 Lemma plus_n_Sm : (n,m:nat) (S (plus n m))=(plus n (S m)).
 Proof.
- Intros m n; Elim m; Simpl; Auto.
+  Intros m n; Elim m; Simpl; Auto.
 Qed.
 Hints Resolve plus_n_Sm : core v62.
 
@@ -100,15 +100,15 @@ Hint eq_mult : core v62 := Resolve (f_equal2 nat nat nat mult).
 
 Lemma mult_n_O : (n:nat) O=(mult n O).
 Proof.
- Induction n; Simpl; Auto.
+  Induction n; Simpl; Auto.
 Qed.
 Hints Resolve mult_n_O : core v62.
 
 Lemma mult_n_Sm : (n,m:nat) (plus (mult n m) n)=(mult n (S m)).
 Proof.
- Intros; Elim n; Simpl; Auto.
- Intros p H; Case H; Elim plus_n_Sm; Apply (f_equal nat nat S).
- Pattern 1 3 m; Elim m; Simpl; Auto.
+  Intros; Elim n; Simpl; Auto.
+  Intros p H; Case H; Elim plus_n_Sm; Apply (f_equal nat nat S).
+  Pattern 1 3 m; Elim m; Simpl; Auto.
 Qed.
 Hints Resolve mult_n_Sm : core v62.
 
@@ -141,7 +141,7 @@ Hints Unfold gt : core v62.
 
 Theorem nat_case : (n:nat)(P:nat->Prop)(P O)->((m:nat)(P (S m)))->(P n).
 Proof.
- Induction n ; Auto.
+  Induction n ; Auto.
 Qed.
 
 (**********************************************************)
@@ -153,6 +153,6 @@ Theorem nat_double_ind : (R:nat->nat->Prop)
      -> ((n,m:nat)(R n m)->(R (S n) (S m)))
      -> (n,m:nat)(R n m).
 Proof.
- Induction n; Auto.
- Induction m; Auto.
+  Induction n; Auto.
+  Induction m; Auto.
 Qed.
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 3de2b086fd..1c41fe1033 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -159,7 +159,7 @@ let start () =
     Lib.init();
     try
       parse_args ();
-      print_header ();
+      if is_verbose() then print_header ();
       init_load_path ();
       inputstate ();
       load_vernac_obj ();