From 6b691bbd2101fd39395c0d2135fd7c06a8915e14 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Fri, 24 Dec 2010 11:53:29 +0100 Subject: Imported Upstream version 8.3pl1 --- theories/Numbers/Natural/BigN/NMake_gen.ml | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) (limited to 'theories/Numbers/Natural/BigN/NMake_gen.ml') 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 _)."; -- cgit v1.2.3