- 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

4 files changed, 7 insertions, 11 deletions

diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 16a95d065c..31465a7a79 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -2105,9 +2105,9 @@ let rec xlate_vernac =
       CT_coercion (local_opt, id_opt, xlate_ident id1,
         xlate_class id2, xlate_class id3)
 
-    (* TypeClasses *) 
+    (* Type Classes *) 
    | VernacDeclareInstance _|VernacContext _|
-	 VernacInstance (_, _, _, _)|VernacClass (_, _, _, _, _) ->
+	 VernacInstance (_, _, _, _, _)|VernacClass (_, _, _, _, _) ->
 	   xlate_error "TODO: Type Classes commands"
 
   | VernacResetName id -> CT_reset (xlate_ident (snd id))
diff --git a/contrib/subtac/subtac.ml b/contrib/subtac/subtac.ml
index ac4b9642e7..1cfe69aa95 100644
--- a/contrib/subtac/subtac.ml
+++ b/contrib/subtac/subtac.ml
@@ -145,8 +145,8 @@ let subtac (loc, command) =
       | VernacAssumption (stre,nl,l) -> 
 	  vernac_assumption env isevars stre l nl
 
-      | VernacInstance (sup, is, props, pri) ->
-	  ignore(Subtac_classes.new_instance sup is props pri)
+      | VernacInstance (glob, sup, is, props, pri) ->
+	  ignore(Subtac_classes.new_instance ~global:glob sup is props pri)
 
       | VernacCoFixpoint (l, b) ->
 	  let _ = trace (str "Building cofixpoint") in
diff --git a/contrib/subtac/subtac_classes.ml b/contrib/subtac/subtac_classes.ml
index 2a8e2e5d90..7ec5d3575f 100644
--- a/contrib/subtac/subtac_classes.ml
+++ b/contrib/subtac/subtac_classes.ml
@@ -100,7 +100,7 @@ let type_class_instance_params isevars env id n ctx inst subst =
 let substitution_of_constrs ctx cstrs =
   List.fold_right2 (fun c (na, _, _) acc -> (na, c) :: acc) cstrs ctx []
 
-let new_instance ctx (instid, bk, cl) props ?(on_free_vars=Classes.default_on_free_vars) pri =
+let new_instance ?(global=false) ctx (instid, bk, cl) props ?(on_free_vars=Classes.default_on_free_vars) pri =
   let env = Global.env() in
   let isevars = ref (Evd.create_evar_defs Evd.empty) in
   let bound = Implicit_quantifiers.ids_of_list (Termops.ids_of_context env) in
@@ -204,12 +204,7 @@ let new_instance ctx (instid, bk, cl) props ?(on_free_vars=Classes.default_on_fr
 (*       1 ctx *)
 (*   in *)
   let hook cst = 
-    let inst = 
-      { is_class = k;
-	is_pri = pri;
-	is_impl = cst;
-      }
-    in
+    let inst = Typeclasses.new_instance k pri global cst in
       Impargs.declare_manual_implicits false (ConstRef cst) false imps;
       Typeclasses.add_instance inst
   in
diff --git a/contrib/subtac/subtac_classes.mli b/contrib/subtac/subtac_classes.mli
index 92a94cda65..99231f585e 100644
--- a/contrib/subtac/subtac_classes.mli
+++ b/contrib/subtac/subtac_classes.mli
@@ -33,6 +33,7 @@ val type_ctx_instance :     Evd.evar_defs ref ->
     (Names.identifier * Term.constr option * Term.constr) list
 
 val new_instance : 
+  ?global:bool ->
   Topconstr.local_binder list ->
   typeclass_constraint ->
   binder_def_list ->