Merge subinstances branch by me and Tom Prince.

This adds two experimental features to the typeclass implementation:
- Path cuts: a way to specify through regular expressions on instance names
search pathes that should be avoided (e.g. [proper_flip proper_flip]).
Regular expression matching is implemented through naïve derivatives.
- Forward hints for subclasses: e.g. [Equivalence -> Reflexive] is no
longer applied backwards, but introducing a specific [Equivalence] in the
environment register a [Reflexive] hint as well. Currently not
backwards-compatible, the next patch will allow to specify direction
of subclasses hints.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14671 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 10 insertions, 4 deletions

diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v
index c30d38186..00a840520 100644
--- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v
@@ -285,7 +285,7 @@ Section Z_2nZ.
 
  (* ** Record of operators on 2 words *)
 
- Global Instance mk_zn2z_ops : ZnZ.Ops (zn2z t) :=
+ Global Instance mk_zn2z_ops : ZnZ.Ops (zn2z t) | 1 :=
   ZnZ.MkOps _ww_digits _ww_zdigits
     to_Z ww_of_pos head0 tail0
     W0 ww_1 ww_Bm1
@@ -305,7 +305,7 @@ Section Z_2nZ.
     sqrt2
     sqrt.
 
- Global Instance mk_zn2z_ops_karatsuba : ZnZ.Ops (zn2z t) :=
+ Global Instance mk_zn2z_ops_karatsuba : ZnZ.Ops (zn2z t) | 2 :=
    ZnZ.MkOps _ww_digits _ww_zdigits
     to_Z ww_of_pos head0 tail0
     W0 ww_1 ww_Bm1
diff --git a/theories/Numbers/Integer/Abstract/ZBits.v b/theories/Numbers/Integer/Abstract/ZBits.v
index 39e9f02c5..92afbcb53 100644
--- a/theories/Numbers/Integer/Abstract/ZBits.v
+++ b/theories/Numbers/Integer/Abstract/ZBits.v
@@ -51,6 +51,8 @@ Qed.
 Definition b2z (b:bool) := if b then 1 else 0.
 Local Coercion b2z : bool >-> t.
 
+Instance b2z_wd : Proper (Logic.eq ==> eq) b2z := _.
+
 Lemma exists_div2 a : exists a' (b:bool), a == 2*a' + b.
 Proof.
  elim (Even_or_Odd a); [intros (a',H)| intros (a',H)].
@@ -84,8 +86,8 @@ Qed.
 
 Lemma testbit_spec' a n : 0<=n -> a.[n] == (a / 2^n) mod 2.
 Proof.
- intro Hn. revert a. apply le_ind with (4:=Hn).
- solve_proper.
+ intro Hn. revert a. apply le_ind with (4:=Hn). 
+   solve_proper.
  intros a. nzsimpl.
  destruct (exists_div2 a) as (a' & b & H). rewrite H at 1.
  rewrite testbit_0_r. apply mod_unique with a'; trivial.
diff --git a/theories/Numbers/Natural/Abstract/NBits.v b/theories/Numbers/Natural/Abstract/NBits.v
index ce720c38c..c66f003ec 100644
--- a/theories/Numbers/Natural/Abstract/NBits.v
+++ b/theories/Numbers/Natural/Abstract/NBits.v
@@ -48,6 +48,9 @@ Qed.
 Definition b2n (b:bool) := if b then 1 else 0.
 Local Coercion b2n : bool >-> t.
 
+Instance b2n_proper : Proper (Logic.eq ==> eq) b2n.
+Proof. solve_proper. Qed.
+
 Lemma exists_div2 a : exists a' (b:bool), a == 2*a' + b.
 Proof.
  elim (Even_or_Odd a); [intros (a',H)| intros (a',H)].
diff --git a/theories/Numbers/Rational/BigQ/QMake.v b/theories/Numbers/Rational/BigQ/QMake.v
index 33267a518..995fbb9ee 100644
--- a/theories/Numbers/Rational/BigQ/QMake.v
+++ b/theories/Numbers/Rational/BigQ/QMake.v
@@ -94,6 +94,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
   Z.spec_gcd N.spec_gcd Zgcd_Zabs Zgcd_1
   spec_Z_of_N spec_Zabs_N
  : nz.
+
  Ltac nzsimpl := autorewrite with nz in *.
 
  Ltac qsimpl := try red; unfold to_Q; simpl; intros;