From 44e7deb7c82ec2ddddf551a227c67a76ccb3009a Mon Sep 17 00:00:00 2001
From: msozeau
Date: Tue, 15 Apr 2008 13:19:33 +0000
Subject: - 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
---
 pretyping/typeclasses.mli | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'pretyping/typeclasses.mli')

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
-- 
cgit v1.2.3