Commit 370f076a authored by François Bobot's avatar François Bobot
Browse files

Remove extraction of BinPos.Pos.compare_cont

parent eaf5c8cf
open BinPosDef
open Datatypes
module Pos =
struct
......@@ -107,11 +106,6 @@ module Pos =
(fun _ -> Farith_Big.one)
p
(** val compare_cont :
comparison -> Farith_Big.big_int -> Farith_Big.big_int -> comparison **)
let rec compare_cont = fun c x y -> Farith_Big.compare_case c Lt Gt x y
(** val sqrtrem_step :
(Farith_Big.big_int -> Farith_Big.big_int) -> (Farith_Big.big_int ->
Farith_Big.big_int) -> (Farith_Big.big_int * mask) ->
......
open BinPosDef
open Datatypes
module Pos :
sig
......@@ -27,9 +26,6 @@ module Pos :
val div2_up : Farith_Big.big_int -> Farith_Big.big_int
val compare_cont :
comparison -> Farith_Big.big_int -> Farith_Big.big_int -> comparison
val sqrtrem_step :
(Farith_Big.big_int -> Farith_Big.big_int) -> (Farith_Big.big_int ->
Farith_Big.big_int) -> (Farith_Big.big_int * mask) ->
......
open BinInt
open BinPos
open Datatypes
open Zpower
......@@ -155,14 +154,19 @@ let coq_SFcompare f1 f2 =
(if s1
then if s2
then (match (Farith_Big.compare_case Eq Lt Gt) e1 e2 with
| Eq -> coq_CompOpp (Pos.compare_cont Eq m1 m2)
| Eq ->
coq_CompOpp
((fun c x y -> Farith_Big.compare_case c Lt Gt x y)
Eq m1 m2)
| Lt -> Gt
| Gt -> Lt)
else Lt
else if s2
then Gt
else (match (Farith_Big.compare_case Eq Lt Gt) e1 e2 with
| Eq -> Pos.compare_cont Eq m1 m2
| Eq ->
(fun c x y -> Farith_Big.compare_case c Lt Gt x y) Eq
m1 m2
| x -> x)))
(** val coq_SFeqb : spec_float -> spec_float -> bool **)
......
open BinInt
open BinPos
open Datatypes
open Zpower
......
......@@ -141,6 +141,8 @@ Extract Inlined Constant Pos.shiftr_nat => "Farith_Big.shiftr".
Extract Inlined Constant Pos.shiftl => "Farith_Big.shiftl".
Extract Inlined Constant Pos.shiftr => "Farith_Big.shiftr".
Extract Inlined Constant BinPos.Pos.compare_cont => "(fun c x y -> Farith_Big.compare_case c Lt Gt x y)".
Extract Inlined Constant N.add => "Farith_Big.add".
Extract Inlined Constant N.succ => "Farith_Big.succ".
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment