Micromega: improvement of the code obtained by extraction

  * In eval_cone and simpl_cone, default patterns were leading
    to duplicated computations. Adaptation of RingMicromega.v
    to prevent that.
  * Use the Ocaml builtin types (lists, pairs, bool, etc) and
    remove the useless conversion functions in mutils.ml and alii.
  * andb was extracted to a correctly lazy but ugly match.
    Let's rather use Ocaml's (&&).

  Remain to be done: take advantage of extraction during the build,
   - either directly if we are using plugins, (no dependency issues)
   - or if we compile statically, at least check later that the
     micromega.ml in the archive and the one auto-generated are in sync.

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

1 files changed, 0 insertions, 17 deletions

diff --git a/plugins/micromega/mutils.ml b/plugins/micromega/mutils.ml
index 03e3999fd..23db2928a 100644
--- a/plugins/micromega/mutils.ml
+++ b/plugins/micromega/mutils.ml
@@ -14,9 +14,6 @@
 
 let debug = false
 
-let fst' (Micromega.Pair(x,y)) = x
-let snd' (Micromega.Pair(x,y)) = y
-
 let map_option f x = 
   match x with
     | None -> None
@@ -225,11 +222,6 @@ struct
 
  let num x = Num.Big_int (z_big_int x)
 
- let rec list elt l =
-  match l with
-   | Nil -> []
-   | Cons(e,l) -> (elt e)::(list elt l)
-
  let q_to_num {qnum = x ; qden = y} = 
   Big_int (z_big_int x) // (Big_int (z_big_int (Zpos y)))
   
@@ -256,10 +248,6 @@ struct
   else if nt = 0 then N0
   else Npos (positive nt)
 
-
-   
-
-   
  let rec index  n =
   if n=1 then XH
   else if n land 1 = 1 then XI (index (n lsr 1))
@@ -279,8 +267,6 @@ struct
     (List.rev (digits_of_int n))
     (XH)
 
-    
-
  let z x = 
   match compare x 0 with
    | 0 -> Z0
@@ -311,9 +297,6 @@ struct
   {Micromega.qnum = bigint (numerator n) ; 
    Micromega.qden = positive_big_int (denominator n)}
 
-
- let list elt l = List.fold_right (fun x l -> Cons(elt x, l)) l Nil
-
 end
 
 module Cmp =