Fix make_exact_entry to allow applying [forall x, P x] hints directly,

avoiding the introduction of eta-redexes. Prioritize hints over intros
in typeclass resolution to profit from that. 
Add a minor fix in coqdoc by F. Garillot.


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

4 files changed, 11 insertions, 14 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 92750094c..b6dc4e598 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -270,22 +270,20 @@ let dummy_goal =
 
 let make_exact_entry pri (c,cty) =
   let cty = strip_outer_cast cty in
-  match kind_of_term cty with
-    | Prod (_,_,_) ->
-	failwith "make_exact_entry"
-    | _ ->
-        let ce = mk_clenv_from dummy_goal (c,cty) in
-	let c' = clenv_type ce in
-	let pat = Pattern.pattern_of_constr c' in
-	(Some (head_of_constr_reference (fst (head_constr cty))),
-	   { pri=(match pri with Some pri -> pri | None -> 0); pat=Some pat; code=Give_exact c })
+  let pat = Pattern.pattern_of_constr cty in
+  let head = 
+    try head_of_constr_reference (fst (head_constr cty)) 
+    with _ -> failwith "make_exact_entry" 
+  in
+    (Some head,
+    { pri=(match pri with Some pri -> pri | None -> 0); pat=Some pat; code=Give_exact c })
 
 let make_apply_entry env sigma (eapply,hnf,verbose) pri (c,cty) =
   let cty = if hnf then hnf_constr env sigma cty else cty in
     match kind_of_term cty with
     | Prod _ ->
         let ce = mk_clenv_from dummy_goal (c,cty) in
-	let c' = clenv_type ce in
+	let c' = clenv_type (* ~reduce:false *) ce in
 	let pat = Pattern.pattern_of_constr c' in
         let hd = (try head_pattern_bound pat
           with BoundPattern -> failwith "make_apply_entry") in
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 4d367ac61..bd632b59a 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -452,7 +452,7 @@ let run_on_evars ?(only_classes=true) ?(st=full_transparent_state) p evm tac =
 	| Some (evm', fk) -> Some (Evd.evars_reset_evd evm' evm, fk)
 	    
 let eauto_tac hints = 
-  fix (or_tac intro_tac (then_tac normevars_tac (hints_tac hints)))
+  fix (or_tac (then_tac normevars_tac (hints_tac hints)) intro_tac)
   
 let eauto ?(only_classes=true) ?st hints g =
   let gl = { it = make_autogoal ~only_classes ?st None g; sigma = project g } in
diff --git a/theories/Sets/Integers.v b/theories/Sets/Integers.v
index 443713211..01d3bda37 100644
--- a/theories/Sets/Integers.v
+++ b/theories/Sets/Integers.v
@@ -79,7 +79,6 @@ Section Integers_sect.
       auto with sets arith.
     apply Inhabited_intro with (x := 0).
       apply Integers_defn.
-      exact le_Order.
   Defined.
 
   Lemma le_total_order : Totally_ordered nat nat_po Integers.
diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll
index 4742a2e5d..4f1406cc8 100644
--- a/tools/coqdoc/cpretty.mll
+++ b/tools/coqdoc/cpretty.mll
@@ -184,10 +184,10 @@
   let check_start_list str =
     let n_dashes = count_dashes str in
     let (n_spaces,_) = count_spaces str in
-      if n_dashes >= 4 then
+      if n_dashes >= 4 && not !Cdglobals.plain_comments then
         Rule
       else
-        if n_dashes = 1 then
+        if n_dashes = 1 && not !Cdglobals.plain_comments then
           List n_spaces
         else
           Neither