Imported Upstream version 8.3pl1upstream/8.3pl1

1 files changed, 5 insertions, 5 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 _).";