From 96157ea08f288ed2f28493696e840d6744efebd7 Mon Sep 17 00:00:00 2001
From: thery
Date: Wed, 21 Nov 2007 08:48:58 +0000
Subject: extensible version

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10328 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Ints/num/QbiMake.v | 7 +------
 theories/Ints/num/QifMake.v | 7 +------
 2 files changed, 2 insertions(+), 12 deletions(-)

diff --git a/theories/Ints/num/QbiMake.v b/theories/Ints/num/QbiMake.v
index fdf8647079..3583c5eece 100644
--- a/theories/Ints/num/QbiMake.v
+++ b/theories/Ints/num/QbiMake.v
@@ -237,12 +237,7 @@ Module Qbi.
   | BigN.N6 _ => false
   | BigN.N7 _ => false
   | BigN.N8 _ => false
-  | BigN.N9 _ => true 
-  | BigN.N10 _ => true
-  | BigN.N11 _ => true
-  | BigN.N12 _ => true
-  | BigN.N13 _ => true
-  | BigN.Nn n _ => true
+  | _         => true 
   end.
  
  Definition do_norm_z z :=
diff --git a/theories/Ints/num/QifMake.v b/theories/Ints/num/QifMake.v
index 5f461aa59b..6539ea6ab5 100644
--- a/theories/Ints/num/QifMake.v
+++ b/theories/Ints/num/QifMake.v
@@ -171,12 +171,7 @@ Module Qif.
   | BigN.N6 _ => false
   | BigN.N7 _ => false
   | BigN.N8 _ => false
-  | BigN.N9 _ => true 
-  | BigN.N10 _ => true
-  | BigN.N11 _ => true
-  | BigN.N12 _ => true
-  | BigN.N13 _ => true
-  | BigN.Nn n _ => true
+  | _         => true 
   end.
 
  Definition do_norm_z z :=
-- 
cgit v1.2.3