- Add "Global" modifier for instances inside sections with the usual

semantics. 
- Add an Equivalence instance for pointwise equality from an
Equivalence on the codomain of a function type, used by default when
comparing functions with the Setoid's ===/equiv.
- Partially fix the auto hint database "add" function where the exact
same lemma could be added twice (happens when doing load for example).


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

2 files changed, 4 insertions, 4 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index b5adc66640..52c4837716 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -93,8 +93,8 @@ let empty_se = ([],[],Btermdn.create ())
 
 let add_tac t (l,l',dn) =
   match t.pat with
-      None -> (insert t l, l', dn)
-    | Some pat -> (l, insert t l', Btermdn.add dn (pat,t))
+      None -> if not (List.mem t l) then (insert t l, l', dn) else (l, l', dn)
+    | Some pat -> if not (List.mem t l') then (l, insert t l', Btermdn.add dn (pat,t)) else (l, l', dn)
 
 
 let lookup_tacs (hdc,c) (l,l',dn) =
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 6b322675c5..a54de8b8a7 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -1367,7 +1367,7 @@ let add_morphism_infer m n =
       let cst = Declare.declare_internal_constant instance_id
 	(Entries.ParameterEntry (instance,false), Decl_kinds.IsAssumption Decl_kinds.Logical)
       in
-	add_instance { is_class = Lazy.force morphism_class ; is_pri = None; is_impl = cst };
+	add_instance (Typeclasses.new_instance (Lazy.force morphism_class) None false cst);
 	declare_projection n instance_id (ConstRef cst)
     else
       let kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Instance in
@@ -1376,7 +1376,7 @@ let add_morphism_infer m n =
 	    Command.start_proof instance_id kind instance 
 	      (fun _ -> function
 		  Libnames.ConstRef cst -> 
-		    add_instance { is_class = Lazy.force morphism_class ; is_pri = None; is_impl = cst };
+		    add_instance (Typeclasses.new_instance (Lazy.force morphism_class) None false cst);
 		    declare_projection n instance_id (ConstRef cst)
 		| _ -> assert false);
 	    Pfedit.by (Tacinterp.interp <:tactic<add_morphism_tactic>>)) ();