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

4 files changed, 18 insertions, 9 deletions

diff --git a/library/impargs.ml b/library/impargs.ml
index 138400953..b5c27f430 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -276,11 +276,11 @@ let compute_manual_implicits env flags t enriching l =
       let l',imp,m =
 	try 
 	  let (b, f) = List.assoc (ExplByName id) l in
-	  List.remove_assoc (ExplByName id) l, merge_imps f imp,Some b
+	  List.remove_assoc (ExplByName id) l, (Some Manual), (Some b)
 	with Not_found ->
 	try 
 	  let (id, (b, f)), l' = assoc_by_pos k l in
-	    l', merge_imps f imp,Some b
+	    l', (Some Manual), (Some b)
 	with Not_found ->
 	  l,imp, if enriching && imp <> None then Some flags.maximal else None
       in
@@ -415,12 +415,12 @@ let list_split_at index l =
     | [] -> failwith "list_split_at: Invalid argument"
   in aux 0 [] l
     
-let merge_impls oimpls impls =
-  let oimpls, newimpls = list_split_at (List.length oimpls - List.length impls) oimpls in
-    oimpls @ (List.map2 (fun orig ni ->
+let merge_impls newimpls oldimpls =
+  let before, after = list_split_at (List.length newimpls - List.length oldimpls) newimpls in
+    before @ (List.map2 (fun orig ni ->
       match orig with
       | Some (_, Manual, _) -> orig
-      | _ -> ni) impls newimpls)
+      | _ -> ni) oldimpls after)
 
 (* Caching implicits *)
 
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' }
 	
diff --git a/test-suite/success/setoid_test2.v b/test-suite/success/setoid_test2.v
index 34fff9d18..b89787bb0 100644
--- a/test-suite/success/setoid_test2.v
+++ b/test-suite/success/setoid_test2.v
@@ -120,7 +120,7 @@ Axiom eqS1: S1 -> S1 -> Prop.
 Axiom SetoidS1 : Setoid_Theory S1 eqS1.
 Add Setoid S1 eqS1 SetoidS1 as S1setoid.
 
-Instance eqS1_default : DefaultRelation S1 eqS1.
+Instance eqS1_default : DefaultRelation eqS1.
 
 Axiom eqS1': S1 -> S1 -> Prop.
 Axiom SetoidS1' : Setoid_Theory S1 eqS1'.
@@ -220,7 +220,7 @@ Axiom eqS1_test8: S1_test8 -> S1_test8 -> Prop.
 Axiom SetoidS1_test8 : Setoid_Theory S1_test8 eqS1_test8.
 Add Setoid S1_test8 eqS1_test8 SetoidS1_test8 as S1_test8setoid.
 
-Instance eqS1_test8_default : DefaultRelation S1_test8 eqS1_test8.
+Instance eqS1_test8_default : DefaultRelation eqS1_test8.
 
 Axiom f_test8 : S2 -> S1_test8.
 Add Morphism f_test8 : f_compat_test8. Admitted.
diff --git a/toplevel/record.ml b/toplevel/record.ml
index ab06673e4..5a9e014d4 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -65,6 +65,11 @@ let typecheck_params_and_fields id t ps fs =
   let env2,impls,newfs,data =
     interp_fields_evars evars env_ar (binders_of_decls fs)
   in
+  let newps = Evarutil.nf_rel_context_evar (Evd.evars_of !evars) newps in
+  let newfs = Evarutil.nf_rel_context_evar (Evd.evars_of !evars) newfs in
+  let ce t = Evarutil.check_evars env0 Evd.empty !evars t in
+    List.iter (fun (n, b, t) -> Option.iter ce b; ce t) newps;
+    List.iter (fun (n, b, t) -> Option.iter ce b; ce t) newfs;
     imps, newps, impls, newfs
 
 let degenerate_decl (na,b,t) =