From 64ac193d372ef8428e85010a862ece55ac011192 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Fri, 27 Jun 2008 15:52:05 +0000
Subject: Enhanced discrimination nets implementation, which can now work with
 goals containing existentials and use transparency information on constants
 (optionally). Only used by the typeclasses eauto engine for now, but could be
 used for other hint bases easily (just switch a boolean). Had to add a new
 "creation" hint to be able to set said boolean upon creation of the
 typeclass_instances hint db. Improve the proof-search algorithm for Morphism,
 up to 10 seconds gained in e.g. Field_theory, Ring_polynom. Added a morphism
 declaration for [compose]. One needs to declare more constants as being
 unfoldable using the [Typeclasses unfold] command so that discrimination is
 done correctly, but that amounts to only 6 declarations in the standard
 library.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11184 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Numbers/Integer/BigZ/BigZ.v       | 2 ++
 theories/Numbers/Integer/BigZ/ZMake.v      | 1 +
 theories/Numbers/Natural/BigN/BigN.v       | 2 ++
 theories/Numbers/Natural/BigN/NMake_gen.ml | 2 +-
 4 files changed, 6 insertions(+), 1 deletion(-)

(limited to 'theories/Numbers')

diff --git a/theories/Numbers/Integer/BigZ/BigZ.v b/theories/Numbers/Integer/BigZ/BigZ.v
index 947dc818e1..bb2c01437d 100644
--- a/theories/Numbers/Integer/BigZ/BigZ.v
+++ b/theories/Numbers/Integer/BigZ/BigZ.v
@@ -102,6 +102,8 @@ 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 cbf6f701f2..5376027ddb 100644
--- a/theories/Numbers/Integer/BigZ/ZMake.v
+++ b/theories/Numbers/Integer/BigZ/ZMake.v
@@ -30,6 +30,7 @@ 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 485480fa04..1e0b45cd2c 100644
--- a/theories/Numbers/Natural/BigN/BigN.v
+++ b/theories/Numbers/Natural/BigN/BigN.v
@@ -76,6 +76,8 @@ 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 0baba94c6d..c360f53dc8 100644
--- a/theories/Numbers/Natural/BigN/NMake_gen.ml
+++ b/theories/Numbers/Natural/BigN/NMake_gen.ml
@@ -139,7 +139,7 @@ let _ =
   pr "";
   pr " Definition %s := %s_." t t;
   pr "";
-
+  pr " Typeclasses unfold %s." t;
   pr " Definition w_0 := w0_op.(znz_0).";
   pr "";
 
-- 
cgit v1.2.3