- 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

1 files changed, 5 insertions, 5 deletions

diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index c091842f04..d35ee54140 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -41,11 +41,11 @@ type typeclass = {
   cl_projs : constant list;
 }
 
-type instance = {
-  is_class: typeclass;
-  is_pri : int option;
-  is_impl: constant;
-}
+type instance
+
+val instance_impl : instance -> constant
+
+val new_instance : typeclass -> int option -> bool -> constant -> instance
   
 val instances : global_reference -> instance list
 val typeclasses : unit -> typeclass list