diff options
Diffstat (limited to 'theories/Numbers/Natural')
| -rw-r--r-- | theories/Numbers/Natural/BigN/NMake_gen.ml | 10 | ||||
| -rw-r--r-- | theories/Numbers/Natural/BigN/Nbasic.v | 11 |
2 files changed, 7 insertions, 14 deletions
diff --git a/theories/Numbers/Natural/BigN/NMake_gen.ml b/theories/Numbers/Natural/BigN/NMake_gen.ml index 8f6c59fd..052d9c92 100644 --- a/theories/Numbers/Natural/BigN/NMake_gen.ml +++ b/theories/Numbers/Natural/BigN/NMake_gen.ml @@ -8,7 +8,7 @@ (* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *) (************************************************************************) -(*i $Id: NMake_gen.ml 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: NMake_gen.ml 13734 2010-12-21 18:21:56Z letouzey $ i*) (*S NMake_gen.ml : this file generates NMake.v *) @@ -1299,7 +1299,7 @@ let _ = pr " (iter _"; for i = 0 to size do pr " compare_%i" i; - pr " (fun n x y => opp_compare (comparen_%i (S n) y x))" i; + pr " (fun n x y => CompOpp (comparen_%i (S n) y x))" i; pr " (fun n => comparen_%i (S n))" i; done; pr " comparenm)."; @@ -1339,9 +1339,9 @@ let _ = pp " Let spec_opp_compare: forall c (u v: Z),"; pp " match c with Eq => u = v | Lt => u < v | Gt => u > v end ->"; - pp " match opp_compare c with Eq => v = u | Lt => v < u | Gt => v > u end."; + pp " match CompOpp c with Eq => v = u | Lt => v < u | Gt => v > u end."; pp " Proof."; - pp " intros c u v; case c; unfold opp_compare; auto with zarith."; + pp " intros c u v; case c; unfold CompOpp; auto with zarith."; pp " Qed."; pp ""; @@ -1362,7 +1362,7 @@ let _ = pp " end)"; for i = 0 to size do pp " compare_%i" i; - pp " (fun n x y => opp_compare (comparen_%i (S n) y x))" i; + pp " (fun n x y => CompOpp (comparen_%i (S n) y x))" i; pp " (fun n => comparen_%i (S n)) _ _ _" i; done; pp " comparenm _)."; diff --git a/theories/Numbers/Natural/BigN/Nbasic.v b/theories/Numbers/Natural/BigN/Nbasic.v index a531b92e..3741c95d 100644 --- a/theories/Numbers/Natural/BigN/Nbasic.v +++ b/theories/Numbers/Natural/BigN/Nbasic.v @@ -8,7 +8,7 @@ (* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *) (************************************************************************) -(*i $Id: Nbasic.v 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: Nbasic.v 13734 2010-12-21 18:21:56Z letouzey $ i*) Require Import ZArith. Require Import BigNumPrelude. @@ -260,13 +260,6 @@ Section ReduceRec. End ReduceRec. -Definition opp_compare cmp := - match cmp with - | Lt => Gt - | Eq => Eq - | Gt => Lt - end. - Section CompareRec. Variable wm w : Type. @@ -447,7 +440,7 @@ End AddS. | Lt => y < x | Gt => y > x end -> - match opp_compare u with + match CompOpp u with | Eq => x = y | Lt => x < y | Gt => x > y |