Keyed unification option, compiling the whole standard library

(but deactivated still).

Set Keyed Unification to activate the option, which changes
subterm selection to _always_ use full conversion _after_ finding a
subterm whose head/key matches the key of the term we're looking for.
This applies to rewrite and higher-order unification in
apply/elim/destruct.

Most proof scripts already abide by these semantics. For those that
don't, it's usually only a matter of using:

Declare Equivalent Keys f g.

This make keyed unification consider f and g to match as keys.
This takes care of most cases of abbreviations: typically Def foo :=
bar and rewriting with a bar-headed lhs in a goal mentioning foo works
once they're set equivalent.
For canonical structures, these hints should be automatically declared.

For non-global-reference headed terms, the key is the constructor name
(Sort, Prod...). Evars and metas are no keys.

INCOMPATIBILITIES:
In FMapFullAVL, a Function definition doesn't go through with keyed
unification on.

22 files changed, 174 insertions, 72 deletions

diff --git a/library/impargs.ml b/library/impargs.ml
index cbbb2cea9..d88d6f106 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -542,17 +542,9 @@ let discharge_implicits (_,(req,l)) =
   | ImplInteractive (ref,flags,exp) ->
     (try
       let vars = section_segment_of_reference ref in
-      (* let isproj =  *)
-      (* 	 match ref with *)
-      (* 	 | ConstRef cst -> is_projection cst (Global.env ()) *)
-      (* 	 | _ -> false *)
-      (* in *)
       let ref' = if isVarRef ref then ref else pop_global_reference ref in
       let extra_impls = impls_of_context vars in
-      let l' = 
-	(* if isproj then [ref',snd (List.hd l)] *)
-	(* else *)
-	  [ref', List.map (add_section_impls vars extra_impls) (snd (List.hd l))] in
+      let l' = [ref', List.map (add_section_impls vars extra_impls) (snd (List.hd l))] in
       Some (ImplInteractive (ref',flags,exp),l')
     with Not_found -> (* ref not defined in this section *) Some (req,l))
   | ImplConstant (con,flags) ->
@@ -560,10 +552,7 @@ let discharge_implicits (_,(req,l)) =
       let con' = pop_con con in
       let vars,_,_ = section_segment_of_constant con in
       let extra_impls = impls_of_context vars in
-      let newimpls = 
-	(* if is_projection con (Global.env()) then (snd (List.hd l)) *)
-	(* else *) List.map (add_section_impls vars extra_impls) (snd (List.hd l))
-      in
+      let newimpls = List.map (add_section_impls vars extra_impls) (snd (List.hd l)) in
       let l' = [ConstRef con',newimpls] in
 	Some (ImplConstant (con',flags),l')
     with Not_found -> (* con not defined in this section *) Some (req,l))
diff --git a/library/keys.ml b/library/keys.ml
index c661e67fb..e4af0380b 100644
--- a/library/keys.ml
+++ b/library/keys.ml
@@ -1,8 +1,17 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(** Keys for unification and indexing *)
+
 open Globnames
 open Term
 open Libobject
 
-
 type key = 
   | KGlob of global_reference
   | KLam 
@@ -51,16 +60,23 @@ end
 module Keymap = HMap.Make(KeyOrdered)
 module Keyset = Keymap.Set
 
-(* Union-find structure for references to be considered equivalent *)
+(* Mapping structure for references to be considered equivalent *)
+
+type keys = Keyset.t Keymap.t
 
-module KeyUF = Unionfind.Make(Keyset)(Keymap)
+let keys = Summary.ref Keymap.empty ~name:"Keys_decl"
 
-let keys = (* Summary.ref ( *)KeyUF.create ()(* ) ~name:"Keys_decl" *)
+let add_kv k v m =
+  try Keymap.modify k (fun k' vs -> Keyset.add v vs) m
+  with Not_found -> Keymap.add k (Keyset.singleton v) m
 
-let add_keys k v = KeyUF.union k v keys
+let add_keys k v = 
+  keys := add_kv k v (add_kv v k !keys)
 
 let equiv_keys k k' =
-  k == k' || KeyUF.find k keys == KeyUF.find k' keys
+  k == k' || KeyOrdered.equal k k' ||
+    try Keyset.mem k' (Keymap.find k !keys)
+    with Not_found -> false
 
 (** Registration of keys as an object *)
 
@@ -79,8 +95,8 @@ let subst_keys (subst,(k,k')) =
   (subst_key subst k, subst_key subst k')
 
 let discharge_key = function
-  | KGlob (VarRef _) -> None
-  | KGlob g -> Some (KGlob (pop_global_reference g))
+  | KGlob g when Lib.is_in_section g ->
+    if isVarRef g then None else Some (KGlob (pop_global_reference g))
   | x -> Some x
 
 let discharge_keys (_,(k,k')) =
@@ -101,26 +117,54 @@ let inKeys : key_obj -> obj =
     discharge_function = discharge_keys;
     rebuild_function = rebuild_keys }
 
-let declare_keys ref ref' =
+let declare_equiv_keys ref ref' =
   Lib.add_anonymous_leaf (inKeys (ref,ref'))
 
-let rec constr_key c =
+let constr_key c =
   let open Globnames in 
-  match kind_of_term c with
-  | Const (c, _) -> KGlob (ConstRef c)
-  | Ind (i, u) -> KGlob (IndRef i)
-  | Construct (c,u) -> KGlob (ConstructRef c)
-  | Var id -> KGlob (VarRef id)
-  | App (f, _) -> constr_key f
-  | Proj (p, _) -> KGlob (ConstRef p)
-  | Cast (p, _, _) -> constr_key p
-  | Lambda _ -> KLam 
-  | Prod _ -> KProd
-  | Case _ -> KCase
-  | Fix _ -> KFix
-  | CoFix _ -> KCoFix
-  | Rel _ -> KRel
-  | Meta _ -> KMeta
-  | Evar _ -> KEvar
-  | Sort _ -> KSort 
-  | LetIn _ -> KLet
+  try 
+    let rec aux k = 
+      match kind_of_term k with
+      | Const (c, _) -> KGlob (ConstRef c)
+      | Ind (i, u) -> KGlob (IndRef i)
+      | Construct (c,u) -> KGlob (ConstructRef c)
+      | Var id -> KGlob (VarRef id)
+      | App (f, _) -> aux f
+      | Proj (p, _) -> KGlob (ConstRef (Names.Projection.constant p))
+      | Cast (p, _, _) -> aux p
+      | Lambda _ -> KLam 
+      | Prod _ -> KProd
+      | Case _ -> KCase
+      | Fix _ -> KFix
+      | CoFix _ -> KCoFix
+      | Rel _ -> KRel
+      | Meta _ -> raise Not_found
+      | Evar _ -> raise Not_found
+      | Sort _ -> KSort 
+      | LetIn _ -> KLet
+    in Some (aux c)
+  with Not_found -> None
+
+open Pp
+
+let pr_key pr_global = function
+  | KGlob gr -> pr_global gr
+  | KLam -> str"Lambda"
+  | KLet -> str"Let"
+  | KProd -> str"Product"
+  | KSort -> str"Sort"
+  | KEvar -> str"Evar"
+  | KCase -> str"Case"
+  | KFix -> str"Fix"
+  | KCoFix -> str"CoFix"
+  | KRel -> str"Rel"
+  | KMeta -> str"Meta"
+
+let pr_keyset pr_global v = 
+  prlist_with_sep spc (pr_key pr_global) (Keyset.elements v)
+
+let pr_mapping pr_global k v = 
+  pr_key pr_global k ++ str" <-> " ++ pr_keyset pr_global v
+
+let pr_keys pr_global =
+  Keymap.fold (fun k v acc -> pr_mapping pr_global k v ++ fnl () ++ acc) !keys (mt())
diff --git a/library/keys.mli b/library/keys.mli
index 87ba45558..36789c83b 100644
--- a/library/keys.mli
+++ b/library/keys.mli
@@ -10,11 +10,14 @@ open Globnames
 
 type key
 
-val declare_keys : key -> key -> unit
+val declare_equiv_keys : key -> key -> unit
 (** Declare two keys as being equivalent. *)
 
 val equiv_keys : key -> key -> bool
 (** Check equivalence of keys. *)
 
-val constr_key : Term.constr -> key
+val constr_key : Term.constr -> key option
 (** Compute the head key of a term. *)
+
+val pr_keys : (global_reference -> Pp.std_ppcmds) -> Pp.std_ppcmds
+(** Pretty-print the mapping *)
diff --git a/plugins/micromega/ZCoeff.v b/plugins/micromega/ZCoeff.v
index d65c60167..50197872c 100644
--- a/plugins/micromega/ZCoeff.v
+++ b/plugins/micromega/ZCoeff.v
@@ -93,6 +93,7 @@ Ltac le_less := rewrite (Rle_lt_eq sor); left; try assumption.
 Ltac le_equal := rewrite (Rle_lt_eq sor); right; try reflexivity; try assumption.
 
 Definition gen_order_phi_Z : Z -> R := gen_phiZ 0 1 rplus rtimes ropp.
+Declare Equivalent Keys gen_order_phi_Z gen_phiZ.
 
 Notation phi_pos := (gen_phiPOS 1 rplus rtimes).
 Notation phi_pos1 := (gen_phiPOS1 1 rplus rtimes).
diff --git a/plugins/micromega/ZMicromega.v b/plugins/micromega/ZMicromega.v
index 78837d4cd..c982db393 100644
--- a/plugins/micromega/ZMicromega.v
+++ b/plugins/micromega/ZMicromega.v
@@ -155,12 +155,16 @@ Proof.
 Qed.
 
 Definition psub  := psub Z0  Z.add Z.sub Z.opp Zeq_bool.
+Declare Equivalent Keys psub RingMicromega.psub.
 
 Definition padd  := padd Z0  Z.add Zeq_bool.
+Declare Equivalent Keys padd RingMicromega.padd.
 
 Definition norm  := norm 0 1 Z.add Z.mul Z.sub Z.opp Zeq_bool.
+Declare Equivalent Keys norm RingMicromega.norm.
 
 Definition eval_pol := eval_pol Z.add Z.mul (fun x => x).
+Declare Equivalent Keys eval_pol RingMicromega.eval_pol.
 
 Lemma eval_pol_sub : forall env lhs rhs, eval_pol env (psub  lhs rhs) = eval_pol env lhs - eval_pol env rhs.
 Proof.
@@ -202,11 +206,10 @@ Definition normalise (t:Formula Z) : cnf (NFormula Z) :=
 
 Lemma normalise_correct : forall env t, eval_cnf eval_nformula env (normalise t) <-> Zeval_formula env t.
 Proof.
-  Opaque padd.
-  unfold normalise, xnormalise  ; simpl; intros env t.
+  unfold normalise, xnormalise; cbn -[padd]; intros env t.
   rewrite Zeval_formula_compat.
   unfold eval_cnf, eval_clause.
-  destruct t as [lhs o rhs]; case_eq o; simpl;
+  destruct t as [lhs o rhs]; case_eq o; cbn -[padd];
     repeat rewrite eval_pol_sub;
       repeat rewrite eval_pol_add;
       repeat rewrite <- eval_pol_norm ; simpl in *;
@@ -216,7 +219,6 @@ Proof.
   generalize (eval_pexpr  Z.add Z.mul Z.sub Z.opp (fun x : Z => x)
     (fun x : N => x) (pow_N 1 Z.mul) env rhs) ; intros z1 z2 ; intros ; subst;
     intuition (auto with zarith).
-  Transparent padd.
 Qed.
 
 Definition xnegate (t:RingMicromega.Formula Z) : list (NFormula Z)  :=
diff --git a/plugins/setoid_ring/Field_theory.v b/plugins/setoid_ring/Field_theory.v
index ad7fbd871..16f9b9723 100644
--- a/plugins/setoid_ring/Field_theory.v
+++ b/plugins/setoid_ring/Field_theory.v
@@ -1168,7 +1168,8 @@ induction fe; simpl condition; rewrite ?PCond_cons, ?PCond_app; simpl;
   assert (U2 := split_ok_r (num F1) (num F2) l).
   assert (U3 := split_ok_l (denum F1) (denum F2) l).
   assert (U4 := split_ok_r (denum F1) (denum F2) l).
-  rewrite (IHfe1 Hc2), (IHfe2 Hc3), U1, U2, U3, U4; apply rdiv7b;
+  rewrite (IHfe1 Hc2), (IHfe2 Hc3), U1, U2, U3, U4.
+  simpl in U2, U3, U4. apply rdiv7b;
    rewrite <- ?U2, <- ?U3, <- ?U4; try apply Pcond_Fnorm; trivial.
 
 - rewrite !NPEpow_ok. simpl. rewrite !rpow_pow, (IHfe Hc).
@@ -1274,6 +1275,9 @@ Qed.
 (* simplify a field equation : generate the crossproduct and simplify
    polynomials *)
 
+(** This allows rewriting modulo the simplification of PEeval on PMul *)
+Declare Equivalent Keys PEeval rmul.
+
 Theorem Field_simplify_eq_correct :
  forall n l lpe fe1 fe2,
     Ninterp_PElist l lpe ->
@@ -1294,8 +1298,7 @@ rewrite (split_ok_r (denum nfe1) (denum nfe2) l), eq3.
 simpl.
 rewrite !rmul_assoc.
 apply rmul_ext; trivial.
-rewrite
- (ring_rw_correct n lpe l Hlpe Logic.eq_refl (num nfe1 * right den) Logic.eq_refl),
+rewrite (ring_rw_correct n lpe l Hlpe Logic.eq_refl (num nfe1 * right den) Logic.eq_refl),
  (ring_rw_correct n lpe l Hlpe Logic.eq_refl (num nfe2 * left den) Logic.eq_refl).
 rewrite Hlmp.
 apply Hcrossprod.
diff --git a/plugins/setoid_ring/Ncring_initial.v b/plugins/setoid_ring/Ncring_initial.v
index 528ad4f17..40748c044 100644
--- a/plugins/setoid_ring/Ncring_initial.v
+++ b/plugins/setoid_ring/Ncring_initial.v
@@ -192,6 +192,7 @@ Lemma gen_phiZ_opp : forall x, [- x] == - [x].
  Lemma gen_phiZ_ext : forall x y : Z, x = y -> [x] == [y].
  Proof. intros;subst;reflexivity. Qed.
 
+Declare Equivalent Keys bracket gen_phiZ.
 (*proof that [.] satisfies morphism specifications*)
 Global Instance gen_phiZ_morph :
 (@Ring_morphism (Z:Type) R _ _ _ _ _ _ _ Zops Zr _ _ _ _ _ _ _ _ _ gen_phiZ) . (* beurk!*)
diff --git a/plugins/setoid_ring/Ring_polynom.v b/plugins/setoid_ring/Ring_polynom.v
index 5ec73950b..3e0e931b6 100644
--- a/plugins/setoid_ring/Ring_polynom.v
+++ b/plugins/setoid_ring/Ring_polynom.v
@@ -1033,16 +1033,18 @@ Section POWER.
   now destruct pe.
   Qed.
 
+  Arguments norm_aux !pe : simpl nomatch.
+
   Lemma norm_aux_spec l pe :
     PEeval l pe == (norm_aux pe)@l.
   Proof.
    intros.
-   induction pe.
-   - now rewrite (morph0 CRmorph).
+   induction pe; cbn.
+   - now rewrite (morph0 CRmorph). 
    - now rewrite (morph1 CRmorph).
    - reflexivity.
    - apply mkX_ok.
-   - simpl PEeval. rewrite IHpe1, IHpe2.
+   - rewrite IHpe1, IHpe2.
      assert (H1 := norm_aux_PEopp pe1).
      assert (H2 := norm_aux_PEopp pe2).
      rewrite norm_aux_PEadd.
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index efa64ca1e..735d4b68a 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -1457,11 +1457,17 @@ let make_abstraction env evd ccl abs =
       make_abstraction_core name
         (make_eq_test env evd c) (evd,c) ty occs check_occs env ccl
 
-let keyed_unify env evd kop cl = 
-  if not !keyed_unification then true
-  else
-    let k2 = Keys.constr_key cl in
-      Keys.equiv_keys kop k2
+let keyed_unify env evd kop = 
+  if not !keyed_unification then fun cl -> true
+  else 
+    match kop with 
+    | None -> fun _ -> true
+    | Some kop ->
+      fun cl ->
+	let kc = Keys.constr_key cl in
+	  match kc with
+	  | None -> false
+	  | Some kc -> Keys.equiv_keys kop kc
 
 (* Tries to find an instance of term [cl] in term [op].
    Unifies [cl] to every subterm of [op] until it finds a match.
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 0647fa813..ffd164d16 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -994,3 +994,19 @@ let decompose l c =
 TACTIC EXTEND decompose
 | [ "decompose" "[" ne_constr_list(l) "]" constr(c) ] -> [ decompose l c ]
 END
+
+(** library/keys *)
+
+VERNAC COMMAND EXTEND Declare_keys CLASSIFIED AS SIDEFF
+| [ "Declare" "Equivalent" "Keys" constr(c) constr(c') ] -> [ 
+  let it c = snd (Constrintern.interp_open_constr (Global.env ()) Evd.empty c) in 
+  let k1 = Keys.constr_key (it c) in
+  let k2 = Keys.constr_key (it c') in
+    match k1, k2 with
+    | Some k1, Some k2 -> Keys.declare_equiv_keys k1 k2
+    | _ -> () ]
+END
+
+VERNAC COMMAND EXTEND Print_keys CLASSIFIED AS QUERY
+| [ "Print" "Equivalent" "Keys" ] -> [ msg_info (Keys.pr_keys Printer.pr_global) ]
+END
diff --git a/test-suite/bugs/opened/1596.v b/test-suite/bugs/opened/1596.v
index 91cd09910..7c5dc4167 100644
--- a/test-suite/bugs/opened/1596.v
+++ b/test-suite/bugs/opened/1596.v
@@ -1,10 +1,11 @@
-
 Require Import Relations.
 Require Import FSets.
 Require Import Arith.
 Require Import Omega.
 Unset Standard Proposition Elimination Names.
 
+Set Keyed Unification.
+
 Lemma Bool_elim_bool : forall (b:bool),b=true \/ b=false.
   destruct b;try tauto.
 Qed.
@@ -255,9 +256,6 @@ n).
     induction m;simpl;intro.
     elim (Bool_elim_bool (H.mem (MessageSpi.MNam n,n0) h));intros.
     apply SynInc;apply H.mem_2;trivial.
-    
-    Fail rewrite H in H0. (* !! impossible here !! *)
-Abort.
-(*    discriminate H0.
-  Qed.*)
+    rewrite H in H0. discriminate. (* !! impossible here !! *)
+  Qed.
 End B.
\ No newline at end of file
diff --git a/test-suite/success/keyedrewrite.v b/test-suite/success/keyedrewrite.v
index 438613b44..c99b16e2b 100644
--- a/test-suite/success/keyedrewrite.v
+++ b/test-suite/success/keyedrewrite.v
@@ -1 +1,22 @@
-Lemma foo : 
\ No newline at end of file
+Section foo.
+Variable f : nat -> nat. 
+
+Definition g := f.
+
+Variable lem : g 0 = 0.
+
+Goal f 0 = 0.
+Proof.
+  Fail rewrite lem.
+Abort.
+
+Declare Equivalent Keys @g @f.
+(** Now f and g are considered equivalent heads for subterm selection *)
+Goal f 0 = 0.
+Proof.
+  rewrite lem.
+  reflexivity.
+Qed.
+
+Print Equivalent Keys.
+End foo.
diff --git a/theories/FSets/FMapFullAVL.v b/theories/FSets/FMapFullAVL.v
index dea23d68c..a7be32328 100644
--- a/theories/FSets/FMapFullAVL.v
+++ b/theories/FSets/FMapFullAVL.v
@@ -674,6 +674,8 @@ Module IntMake_ord (I:Int)(X: OrderedType)(D : OrderedType) <:
   Definition cardinal_e_2 ee :=
    (cardinal_e (fst ee) + cardinal_e (snd ee))%nat.
 
+  Local Unset Keyed Unification.
+
   Function compare_aux (ee:Raw.enumeration D.t * Raw.enumeration D.t)
    { measure cardinal_e_2 ee } : comparison :=
   match ee with
diff --git a/theories/FSets/FSetCompat.v b/theories/FSets/FSetCompat.v
index 6b3d86d39..b1769da3d 100644
--- a/theories/FSets/FSetCompat.v
+++ b/theories/FSets/FSetCompat.v
@@ -283,6 +283,8 @@ Module Update_WSets
 
   Lemma is_empty_spec : is_empty s = true <-> Empty s.
   Proof. intros; symmetry; apply MF.is_empty_iff. Qed.
+  
+  Declare Equivalent Keys In M.In.
 
   Lemma add_spec : In y (add x s) <-> E.eq y x \/ In y s.
   Proof. intros. rewrite MF.add_iff. intuition. Qed.
diff --git a/theories/FSets/FSetPositive.v b/theories/FSets/FSetPositive.v
index 88011ff1c..7398c6d65 100644
--- a/theories/FSets/FSetPositive.v
+++ b/theories/FSets/FSetPositive.v
@@ -306,6 +306,9 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
   Notation "s  [<=]  t" := (Subset s t) (at level 70, no associativity).
 
   Definition eq := Equal.
+
+  Declare Equivalent Keys Equal eq.
+
   Definition lt m m' := compare_fun m m' = Lt.
 
   (** Specification of [In] *)
diff --git a/theories/MSets/MSetGenTree.v b/theories/MSets/MSetGenTree.v
index 901574235..d1d9897fb 100644
--- a/theories/MSets/MSetGenTree.v
+++ b/theories/MSets/MSetGenTree.v
@@ -970,6 +970,8 @@ Definition lt (s1 s2 : tree) : Prop :=
  exists s1' s2', Ok s1' /\ Ok s2' /\ eq s1 s1' /\ eq s2 s2'
    /\ L.lt (elements s1') (elements s2').
 
+Declare Equivalent Keys L.eq equivlistA.
+
 Instance lt_strorder : StrictOrder lt.
 Proof.
  split.
diff --git a/theories/Numbers/Cyclic/Abstract/NZCyclic.v b/theories/Numbers/Cyclic/Abstract/NZCyclic.v
index 1d5b78ec4..c9f3a774d 100644
--- a/theories/Numbers/Cyclic/Abstract/NZCyclic.v
+++ b/theories/Numbers/Cyclic/Abstract/NZCyclic.v
@@ -126,9 +126,7 @@ Let B (n : Z) := A (ZnZ.of_Z n).
 
 Lemma B0 : B 0.
 Proof.
-unfold B.
-setoid_replace (ZnZ.of_Z 0) with zero. assumption.
-red; zify. apply ZnZ.of_Z_correct. auto using gt_wB_0 with zarith.
+unfold B. apply A0.
 Qed.
 
 Lemma BS : forall n : Z, 0 <= n -> n < wB - 1 -> B n -> B (n + 1).
diff --git a/theories/Numbers/Natural/BigN/NMake_gen.ml b/theories/Numbers/Natural/BigN/NMake_gen.ml
index 8df4b7c64..dc35d087b 100644
--- a/theories/Numbers/Natural/BigN/NMake_gen.ml
+++ b/theories/Numbers/Natural/BigN/NMake_gen.ml
@@ -961,6 +961,11 @@ pr "  end.";
 pr "";
 
 pr " Ltac unfold_red := unfold reduce, %s." (iter_name 1 size "reduce_" ",");
+pr "";
+for i = 0 to size do
+pr " Declare Equivalent Keys reduce reduce_%i." i;
+done;
+pr " Declare Equivalent Keys reduce_n reduce_%i." (size + 1);
 
 pr "
  Ltac solve_red :=
diff --git a/theories/Numbers/Natural/BigN/Nbasic.v b/theories/Numbers/Natural/BigN/Nbasic.v
index 161f523ca..e8a9940bd 100644
--- a/theories/Numbers/Natural/BigN/Nbasic.v
+++ b/theories/Numbers/Natural/BigN/Nbasic.v
@@ -320,6 +320,7 @@ Section CompareRec.
  Let double_to_Z_pos: forall n x, 0 <= double_to_Z n x < double_wB n :=
    (spec_double_to_Z wm_base wm_to_Z wm_to_Z_pos).
 
+ Declare Equivalent Keys compare0_mn compare0_m.
 
  Lemma spec_compare0_mn: forall n x,
    compare0_mn n x = (0 ?= double_to_Z n x).
diff --git a/theories/Numbers/Rational/BigQ/BigQ.v b/theories/Numbers/Rational/BigQ/BigQ.v
index e866a52d6..b304b339b 100644
--- a/theories/Numbers/Rational/BigQ/BigQ.v
+++ b/theories/Numbers/Rational/BigQ/BigQ.v
@@ -88,6 +88,8 @@ exact BigQ.add_opp_diag_r. exact BigQ.neq_1_0.
 exact BigQ.div_mul_inv. exact BigQ.mul_inv_diag_l.
 Qed.
 
+Declare Equivalent Keys pow_N pow_pos.
+
 Lemma BigQpowerth :
  power_theory 1 BigQ.mul BigQ.eq Z.of_N BigQ.power.
 Proof.
diff --git a/theories/Reals/Binomial.v b/theories/Reals/Binomial.v
index ad076c488..16f2661fe 100644
--- a/theories/Reals/Binomial.v
+++ b/theories/Reals/Binomial.v
@@ -172,13 +172,12 @@ Proof.
   apply sum_eq.
   intros; apply H1.
   unfold N; apply le_lt_trans with n; [ assumption | apply lt_n_Sn ].
-  intros; unfold Bn, Cn.
-  replace (S N - S i)%nat with (N - i)%nat; reflexivity.
+  reflexivity.
   unfold An; fold N; rewrite <- minus_n_n; rewrite H0;
     simpl; ring.
   apply sum_eq.
-  intros; unfold An, Bn; replace (S N - S i)%nat with (N - i)%nat;
-    [ idtac | reflexivity ].
+  intros; unfold An, Bn.
+  change (S N - S i)%nat with (N - i)%nat.
   rewrite <- pascal;
     [ ring
       | apply le_lt_trans with n; [ assumption | unfold N; apply lt_n_Sn ] ].
diff --git a/theories/Reals/Rlimit.v b/theories/Reals/Rlimit.v
index 375cc2752..cf7b91af8 100644
--- a/theories/Reals/Rlimit.v
+++ b/theories/Reals/Rlimit.v
@@ -174,6 +174,8 @@ Definition limit_in (X X':Metric_Space) (f:Base X -> Base X')
 Definition R_met : Metric_Space :=
   Build_Metric_Space R R_dist R_dist_pos R_dist_sym R_dist_refl R_dist_tri.
 
+Declare Equivalent Keys dist R_dist.
+
 (*******************************)
 (** *      Limit 1 arg         *)
 (*******************************)