Fix implicit arguments in sections bug and check for resolution of evars when

defining records. Fix test-suite script because of new implicit argument
setting for DefaultRelation. Fix regression in auto, changing the order
of tried lemmas.


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

1 files changed, 5 insertions, 1 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 69fe51efa..dfc9a6ad2 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -134,6 +134,10 @@ module Hint_db = struct
     let st = if db.use_dn then Some db.hintdb_state else None in
       lookup_tacs (k,c) st (find k db)
 
+  let is_exact = function 
+    | Give_exact _ -> true
+    | _ -> false
+
   let add_one (k,v) db =
     let st',rebuild =
       match v.code with
@@ -150,7 +154,7 @@ module Hint_db = struct
       else None, db
     in
     let oval = find k db in
-    let pat = if not db.use_dn && v.pri = 0 then None else v.pat in
+    let pat = if not db.use_dn && is_exact v.code then None else v.pat in
       { db with hintdb_map = Constr_map.add k (add_tac pat v dnst oval) db.hintdb_map;
 	hintdb_state = st' }