From e8b2255678a7fa1c140c4a50dca26cc94ac1a6e0 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Tue, 10 Nov 2009 11:19:25 +0000
Subject: Simplification of Numbers, mainly thanks to Include

 - No more nesting of Module and Module Type, we rather use Include.
 - Instead of in-name-qualification like NZeq, we use uniform
   short names + modular qualification like N.eq when necessary.
 - Many simplification of proofs, by some autorewrite for instance
 - In NZOrder, we instantiate an "order" tactic.
 - Some requirements in NZAxioms were superfluous: compatibility
   of le, min and max could be derived from the rest.
 - NMul removed, since it was containing only an ad-hoc result for
   ZNatPairs, that we've inlined in the proof of mul_wd there.
 - Zdomain removed (was already not compiled), idea of a module
   with eq and eqb reused in DecidableType.BooleanEqualityType.
 - ZBinDefs don't contain any definition now, migrate it to ZBinary.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12489 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Structures/DecidableType2.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'theories/Structures/DecidableType2.v')

diff --git a/theories/Structures/DecidableType2.v b/theories/Structures/DecidableType2.v
index 6a05d9683d..102572b5b0 100644
--- a/theories/Structures/DecidableType2.v
+++ b/theories/Structures/DecidableType2.v
@@ -149,4 +149,4 @@ Module Dec_to_Bool (E:DecidableType) <: BooleanEqualityType.
   auto with *.
   split. discriminate. intro EQ; elim NEQ; auto.
  Qed.
-End Dec_to_Bool.
\ No newline at end of file
+End Dec_to_Bool.
-- 
cgit v1.2.3