- 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

17 files changed, 114 insertions, 75 deletions

diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 16a95d065..31465a7a7 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 ac4b9642e..1cfe69aa9 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 2a8e2e5d9..7ec5d3575 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 92a94cda6..99231f585 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 ->
diff --git a/doc/refman/Setoid.tex b/doc/refman/Setoid.tex
index a5cc6acbf..8bdf6ab0a 100644
--- a/doc/refman/Setoid.tex
+++ b/doc/refman/Setoid.tex
@@ -34,7 +34,8 @@ the previous implementation in several ways:
   morphisms. Again, most of the work is handled in the tactics.
 \item First-class morphisms and signatures. Signatures and morphisms are
   ordinary Coq terms, hence they can be manipulated inside Coq, put
-  inside structures and lemmas about them can be proved inside the system.
+  inside structures and lemmas about them can be proved inside the
+  system. Higher-order morphisms are also allowed.
 \item Performance. The implementation is based on a depth-first search for the first
   solution to a set of constraints which can be as fast as linear in the
   size of the term, and the size of the proof term is linear
@@ -478,10 +479,9 @@ the projections of the setoid relation and of the morphism function
 can be registered as parametric relations and morphisms.
 \begin{cscexample}[First class setoids]
 
-\begin{verbatim}
+\begin{coq_example*}
 Require Export Relation_Definitions.
 Require Import Setoid.
-
 Record Setoid: Type :=
 { car:Type;
   eq:car->car->Prop;
@@ -489,32 +489,21 @@ Record Setoid: Type :=
   sym: symmetric _ eq;
   trans: transitive _ eq
 }.
-
 Add Parametric Relation (s : Setoid) : (@car s) (@eq s)
  reflexivity proved by (refl s)
  symmetry proved by (sym s)
  transitivity proved by (trans s)
 as eq_rel.
-
 Record Morphism (S1 S2:Setoid): Type :=
 { f:car S1 ->car S2;
-  compat: forall (x1 x2: car S1), eq S1 x1 x2 -> eq S2 (f x1) (f x2)
-}.
-
+  compat: forall (x1 x2: car S1), eq S1 x1 x2 -> eq S2 (f x1) (f x2) }.
 Add Parametric Morphism (S1 S2 : Setoid) (M : Morphism S1 S2) :
  (@f S1 S2 M) with signature (@eq S1 ==> @eq S2) as apply_mor.
-Proof.
- apply (compat S1 S2 M).
-Qed.
-
+Proof. apply (compat S1 S2 M). Qed.
 Lemma test: forall (S1 S2:Setoid) (m: Morphism S1 S2)
  (x y: car S1), eq S1 x y -> eq S2 (f _ _ m x) (f _ _ m y).
-Proof.
- intros.
- rewrite H.
- reflexivity.
-Qed.
-\end{verbatim}
+Proof. intros. rewrite H. reflexivity. Qed.
+\end{coq_example*}
 \end{cscexample}
 
 \asection{Tactics enabled on user provided relations}
@@ -652,7 +641,26 @@ will be generated for the surrounding morphism \texttt{m}.
 
 Hence, one can add higher-order combinators as morphisms by providing
 signatures using pointwise extension for the relations on the functional
-arguments. Note that when one does rewriting with a lemma under a binder
+arguments (or whatever subrelation of the pointwise extension).
+For example, one could declare the \texttt{map} combinator on lists as 
+a morphism:
+\begin{coq_eval}
+Require Import List.
+Set Implicit Arguments.
+Inductive list_equiv {A:Type} (eqA : relation A) : relation (list A) :=
+| eq_nil : list_equiv eqA nil nil
+| eq_cons : forall x y, eqA x y -> 
+  forall l l', list_equiv eqA l l' -> list_equiv eqA (x :: l) (y :: l').
+\end{coq_eval}
+\begin{coq_example*}
+Instance [ Equivalence A eqA, Equivalence B eqB ] => 
+  Morphism ((eqA ==> eqB) ==> list_equiv eqA ==> list_equiv eqB) 
+     (@map A B).
+\end{coq_example*}
+
+where \texttt{list\_equiv} implements an equivalence on lists.
+
+Note that when one does rewriting with a lemma under a binder
 using \texttt{setoid\_rewrite}, the application of the lemma may capture
 the bound variable, as the semantics are different from rewrite where
 the lemma is first matched on the whole term. With the new
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 45c16a133..aea0cf27b 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -489,7 +489,8 @@ GEXTEND Gram
       | IDENT "Context"; c = typeclass_context -> 
 	  VernacContext c
 
-      | IDENT "Instance"; sup = OPT [ l = delimited_binders_let ; "=>" -> l ];
+      | global = [ IDENT "Global" -> true | -> false ];
+	 IDENT "Instance"; sup = OPT [ l = delimited_binders_let ; "=>" -> l ];
 	 is = typeclass_constraint ; pri = OPT [ "|"; i = natural -> i ] ; props = typeclass_field_defs ->
 	   let sup = match sup with None -> [] | Some l -> l in
 	   let is = (* We reverse the default binding mode on the right *)
@@ -497,7 +498,7 @@ GEXTEND Gram
 	       n, (match bk with Rawterm.Implicit -> Rawterm.Explicit 
 		 | Rawterm.Explicit -> Rawterm.Implicit), t 
 	   in
-	     VernacInstance (sup, is, props, pri)
+	     VernacInstance (global, sup, is, props, pri)
 
       | IDENT "Existing"; IDENT "Instance"; is = identref -> VernacDeclareInstance is
 
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index a013b4b93..9fe24f4d4 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -706,8 +706,9 @@ let rec pr_vernac = function
 	  prlist_with_sep (fun () -> str";" ++ spc()) 
 	  (fun (lid,oc,c) -> pr_lident_constr ((if oc then str" :>" else str" :") ++ spc()) (lid,c)) props )
 	
- | VernacInstance (sup, (instid, bk, cl), props, pri) -> 
+ | VernacInstance (glob, sup, (instid, bk, cl), props, pri) -> 
      hov 1 (
+       pr_non_globality (not glob) ++
        str"Instance" ++ spc () ++ 
 	 pr_and_type_binders_arg sup ++
 	 str"=>" ++ spc () ++ 
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml
index 396cc6318..48fe40cab 100644
--- a/parsing/prettyp.ml
+++ b/parsing/prettyp.ml
@@ -773,7 +773,7 @@ let print_typeclasses () =
 let pr_instance env i = 
   (*   gallina_print_constant_with_infos i.is_impl *)
   (* lighter *)
-  print_ref false (ConstRef i.is_impl)
+  print_ref false (ConstRef (instance_impl i))
     
 let print_instances r =
   let env = Global.env () in
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 7ce3351a8..045070960 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -47,14 +47,33 @@ type typeclass = {
 
 type typeclasses = (global_reference, typeclass) Gmap.t
 
+type globality = int option
+
 type instance = {
   is_class: typeclass;
   is_pri: int option;
+  is_global: globality;
+  (* Sections where the instance should be redeclared, 
+     Some n for n sections, None for discard at end of section. *)
   is_impl: constant; 
 }
 
 type instances = (global_reference, instance list) Gmap.t
+
+let instance_impl is = is.is_impl
     
+let new_instance cl pri glob impl = 
+  let global =
+    if Lib.sections_are_opened () then 
+      if glob then Some (Lib.sections_depth ())
+      else None
+    else Some 0
+  in
+    { is_class = cl ;
+      is_pri = pri ;
+      is_global = global ;
+      is_impl = impl }
+	
 let classes : typeclasses ref = ref Gmap.empty
 
 let methods : (constant, global_reference) Gmap.t ref = ref Gmap.empty
@@ -158,8 +177,7 @@ let subst (_,subst,(cl,m,inst)) =
     let insts' = 
       list_smartmap (fun is -> 
 	let is' = 
-	  { is_class = cl; 
-	    is_pri = is.is_pri;
+	  { is with is_class = cl; 
 	    is_impl = do_subst_con is.is_impl }
 	in if is' = is then is else is') insts
     in  Gmap.add k insts' instances
@@ -179,19 +197,27 @@ let discharge (_,(cl,m,inst)) =
   let classes = Gmap.map subst_class cl in
   let subst_inst insts =
     List.map (fun is ->
-      { is_impl = Lib.discharge_con is.is_impl;
-	is_pri = is.is_pri;
+      { is with 
+	is_impl = Lib.discharge_con is.is_impl;
 	is_class = Gmap.find (Lib.discharge_global is.is_class.cl_impl) classes; })
       insts;
   in
   let instances = Gmap.map subst_inst inst in
     Some (classes, m, instances)
-  
-let rebuild (_,(cl,m,inst as obj)) =
-  Gmap.iter (fun _ insts -> 
-    List.iter (fun is -> add_instance_hint is.is_impl is.is_pri) insts) 
-    inst;
-  obj
+      
+let rebuild (_,(cl,m,inst)) =
+  let inst = 
+    Gmap.map (fun insts -> 
+      List.fold_left (fun insts is -> 
+	match is.is_global with
+	  | None -> insts
+	  | Some 0 -> is :: insts
+	  | Some n -> 
+	      add_instance_hint is.is_impl is.is_pri;
+	      let is' = { is with is_global = Some (pred n) }
+	      in is' :: insts) [] insts)
+      inst
+  in (cl, m, inst)
 
 let (input,output) = 
   declare_object
@@ -201,7 +227,7 @@ let (input,output) =
       open_function = (fun _ -> load);
       classify_function = (fun (_,x) -> Substitute x);
       discharge_function = discharge;
-(*       rebuild_function = rebuild; *)
+      rebuild_function = rebuild;
       subst_function = subst;
       export_function = (fun x -> Some x) }
 
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index c091842f0..d35ee5414 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
diff --git a/tactics/auto.ml b/tactics/auto.ml
index b5adc6664..52c483771 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 6b322675c..a54de8b8a 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>>)) ();
diff --git a/theories/Classes/Equivalence.v b/theories/Classes/Equivalence.v
index 4f794af3f..6270fb43b 100644
--- a/theories/Classes/Equivalence.v
+++ b/theories/Classes/Equivalence.v
@@ -178,4 +178,14 @@ Section Respecting.
     symmetry. auto.
   Qed.
 
-End Respecting.
\ No newline at end of file
+End Respecting.
+
+(** The default equivalence on function spaces. *)
+
+Program Instance [ Equivalence A eqA ] => 
+  pointwise_equivalence : Equivalence (B -> A) (pointwise_relation eqA).
+
+  Next Obligation.
+  Proof.
+    transitivity (y x0) ; auto.
+  Qed.
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index db87d36ab..0630e75dc 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -42,20 +42,20 @@ let _ =
       Auto.add_hints false [hint_db] 
 	(Vernacexpr.HintsResolve [pri, CAppExpl (dummy_loc, (None, qualid_of_con inst), [])]))
 
-let declare_instance_constant con =
+let declare_instance_constant glob con =
   let instance = Typeops.type_of_constant (Global.env ()) con in
   let _, r = decompose_prod_assum instance in
     match class_of_constr r with
-      | Some tc -> add_instance { is_class = tc ; is_pri = None; is_impl = con }
+      | Some tc -> add_instance (new_instance tc None glob con)
       | None -> error "Constant does not build instances of a declared type class"
 
-let declare_instance idl =
+let declare_instance glob idl =
   let con = 
     try (match global (Ident idl) with
       | ConstRef x -> x
       | _ -> raise Not_found)
     with _ -> error "Instance definition not found"
-  in declare_instance_constant con
+  in declare_instance_constant glob con
 	  
 let mismatched_params env n m = mismatched_ctx_inst env Parameters n m
 (* let mismatched_defs env n m = mismatched_ctx_inst env Definitions n m *)
@@ -128,7 +128,7 @@ let declare_implicit_proj c proj imps sub =
   in 
   let expls = expls @ List.map (function (ExplByPos (i, n), f) -> (ExplByPos (succ len + i, n)), f | _ -> assert(false)) imps in
     if sub then 
-      declare_instance_constant proj;
+      declare_instance_constant true proj;
     Impargs.declare_manual_implicits true (ConstRef proj) true expls
       
 let declare_implicits impls subs cl =
@@ -429,7 +429,7 @@ let fail_on_free_vars = function
       (str"Unbound variables " ++
 	  prlist_with_sep (fun () -> str", ") Nameops.pr_id fvs ++ str".")
 	
-let new_instance ctx (instid, bk, cl) props ?(on_free_vars=default_on_free_vars) 
+let new_instance ?(global=false) ctx (instid, bk, cl) props ?(on_free_vars=default_on_free_vars) 
     ?(tac:Proof_type.tactic option) ?(hook:(Names.constant -> unit) option) pri =
   let env = Global.env() in
   let isevars = ref (Evd.create_evar_defs Evd.empty) in
@@ -439,7 +439,7 @@ let new_instance ctx (instid, bk, cl) props ?(on_free_vars=default_on_free_vars)
     match bk with
       | Implicit ->
 	  let loc, id, par = Implicit_quantifiers.destClassAppExpl cl in
-	  let k = class_info (global id) in
+	  let k = class_info (Nametab.global id) in
 	  let applen = List.fold_left (fun acc (x, y) -> if y = None then succ acc else acc) 0 par in
 	  let needlen = List.fold_left (fun acc (x, y) -> if x = None then succ acc else acc) 0 k.cl_context in
 	    if needlen <> applen then 
@@ -510,7 +510,7 @@ let new_instance ctx (instid, bk, cl) props ?(on_free_vars=default_on_free_vars)
 	  (Entries.ParameterEntry (termtype,false), Decl_kinds.IsAssumption Decl_kinds.Logical)
 	in
 	  Impargs.maybe_declare_manual_implicits false (ConstRef cst) false imps;
-	  Typeclasses.add_instance { is_class = k ; is_pri = None; is_impl = cst };
+	  Typeclasses.add_instance (Typeclasses.new_instance k None false cst);
 	  Command.assumption_message id;
 	  (match hook with Some h -> h cst | None -> ()); id
       end
@@ -544,12 +544,7 @@ let new_instance ctx (instid, bk, cl) props ?(on_free_vars=default_on_free_vars)
 	isevars := Evarutil.nf_evar_defs !isevars;
 	let term = Evarutil.nf_isevar !isevars term 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.maybe_declare_manual_implicits false (ConstRef cst) false imps;
 	    Typeclasses.add_instance inst;
 	    (match hook with Some h -> h cst | None -> ())
@@ -615,7 +610,7 @@ let context ?(hook=fun _ -> ()) l =
 	in
 	  match class_of_constr t with
 	    | Some tc ->
-		(add_instance { is_class = tc ; is_pri = None; is_impl = cst });
+		add_instance (Typeclasses.new_instance tc None false cst);
 		hook (ConstRef cst)
 	    | None -> ()
       else
diff --git a/toplevel/classes.mli b/toplevel/classes.mli
index be0c98743..92bfa9ad5 100644
--- a/toplevel/classes.mli
+++ b/toplevel/classes.mli
@@ -46,6 +46,7 @@ val default_on_free_vars : identifier list -> unit
 val fail_on_free_vars : identifier list -> unit
     
 val new_instance : 
+  ?global:bool -> (* Not global by default. *)
   local_binder list ->
   typeclass_constraint ->
   binder_def_list ->
@@ -60,7 +61,7 @@ val id_of_class : typeclass -> identifier
     
 val context : ?hook:(Libnames.global_reference -> unit) -> typeclass_context -> unit
 
-val declare_instance : identifier located -> unit
+val declare_instance : bool -> identifier located -> unit
 
 val mismatched_params : env -> constr_expr list -> named_context -> 'a
 
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 726d26131..54228e273 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -533,14 +533,14 @@ let vernac_identity_coercion stre id qids qidt =
 let vernac_class id par ar sup props =
   Classes.new_class id par ar sup props
 
-let vernac_instance sup inst props pri =
-  ignore(Classes.new_instance sup inst props pri)
+let vernac_instance glob sup inst props pri =
+  ignore(Classes.new_instance ~global:glob sup inst props pri)
 
 let vernac_context l =
   Classes.context l
 
 let vernac_declare_instance id =
-  Classes.declare_instance id
+  Classes.declare_instance false id
 
 (***********)
 (* Solving *)
@@ -1222,7 +1222,7 @@ let interp c = match c with
   (* Type classes *)
   | VernacClass (id, par, ar, sup, props) -> vernac_class id par ar sup props
 
-  | VernacInstance (sup, inst, props, pri) -> vernac_instance sup inst props pri
+  | VernacInstance (glob, sup, inst, props, pri) -> vernac_instance glob sup inst props pri
   | VernacContext sup -> vernac_context sup
   | VernacDeclareInstance id -> vernac_declare_instance id
 
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 839f3ee46..6b8fcdead 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -233,6 +233,7 @@ type vernac_expr =
 	(lident * bool * constr_expr) list (* props, with substructure hints *)
 	
   | VernacInstance of
+      bool * (* global *)
       local_binder list * (* super *)
 	typeclass_constraint * (* instance name, class name, params *)
 	(lident * lident list * constr_expr) list * (* props *)