Add user syntax for creating hint databases [Create HintDb foo

[discriminated]] with a switch for using the more experimantal dnet impl
for every hint. Also add [Hint Transparent/Opaque] which parameterize
the dnet and the unification flags used by auto/eauto with a particular
database. Document all this. Remove [Typeclasses unfold] directives that
are no longer needed (everything is unfoldable by default) and move to
[Typeclasses Transparent/Opaque] syntax.


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

4 files changed, 0 insertions, 6 deletions

diff --git a/theories/Numbers/Integer/BigZ/BigZ.v b/theories/Numbers/Integer/BigZ/BigZ.v
index 5189a33ef..f7c423ebb 100644
--- a/theories/Numbers/Integer/BigZ/BigZ.v
+++ b/theories/Numbers/Integer/BigZ/BigZ.v
@@ -104,8 +104,6 @@ exact sub_opp.
 exact add_opp.
 Qed.
 
-Typeclasses unfold NZadd NZmul NZsub NZeq.
-
 Add Ring BigZr : BigZring.
 
 (** Todo: tactic translating from [BigZ] to [Z] + omega *)
diff --git a/theories/Numbers/Integer/BigZ/ZMake.v b/theories/Numbers/Integer/BigZ/ZMake.v
index 5376027dd..cbf6f701f 100644
--- a/theories/Numbers/Integer/BigZ/ZMake.v
+++ b/theories/Numbers/Integer/BigZ/ZMake.v
@@ -30,7 +30,6 @@ Module Make (N:NType) <: ZType.
   | Neg : N.t -> t_.
  
  Definition t := t_.
- Typeclasses unfold t.
 
  Definition zero := Pos N.zero.
  Definition one  := Pos N.one.
diff --git a/theories/Numbers/Natural/BigN/BigN.v b/theories/Numbers/Natural/BigN/BigN.v
index 653170e34..40f08356b 100644
--- a/theories/Numbers/Natural/BigN/BigN.v
+++ b/theories/Numbers/Natural/BigN/BigN.v
@@ -78,8 +78,6 @@ exact mul_assoc.
 exact mul_add_distr_r.
 Qed.
 
-Typeclasses unfold NZadd NZsub NZmul.
-
 Add Ring BigNr : BigNring.
 
 (** Todo: tactic translating from [BigN] to [Z] + omega *)
diff --git a/theories/Numbers/Natural/BigN/NMake_gen.ml b/theories/Numbers/Natural/BigN/NMake_gen.ml
index c360f53dc..7424d877b 100644
--- a/theories/Numbers/Natural/BigN/NMake_gen.ml
+++ b/theories/Numbers/Natural/BigN/NMake_gen.ml
@@ -139,7 +139,6 @@ let _ =
   pr "";
   pr " Definition %s := %s_." t t;
   pr "";
-  pr " Typeclasses unfold %s." t;
   pr " Definition w_0 := w0_op.(znz_0).";
   pr "";