From e0d682ec25282a348d35c5b169abafec48555690 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Mon, 20 Aug 2012 18:27:01 +0200
Subject: Imported Upstream version 8.4dfsg

---
 plugins/micromega/coq_micromega.ml | 23 +++++++++++++----------
 1 file changed, 13 insertions(+), 10 deletions(-)

(limited to 'plugins/micromega/coq_micromega.ml')

diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index 8b7ee55b..2020447f 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -300,6 +300,8 @@ struct
      ["Coq";"Reals" ; "Rpow_def"] ;
 ]
 
+  let z_modules = [["Coq";"ZArith";"BinInt"]]
+
   (**
     * Initialization : a large amount of Caml symbols are derived from
     * ZMicromega.v
@@ -309,6 +311,7 @@ struct
   let constant = gen_constant_in_modules "ZMicromega" coq_modules
   let bin_constant = gen_constant_in_modules "ZMicromega" bin_module
   let r_constant = gen_constant_in_modules "ZMicromega" r_modules
+  let z_constant = gen_constant_in_modules "ZMicromega" z_modules
   (* let constant = gen_constant_in_modules "Omicron" coq_modules *)
 
   let coq_and = lazy (init_constant "and")
@@ -371,17 +374,17 @@ struct
   let coq_cutProof = lazy (constant "CutProof")
   let coq_enumProof = lazy (constant "EnumProof")
 
-  let coq_Zgt = lazy (constant "Zgt")
-  let coq_Zge = lazy (constant "Zge")
-  let coq_Zle = lazy (constant "Zle")
-  let coq_Zlt = lazy (constant "Zlt")
+  let coq_Zgt = lazy (z_constant "Z.gt")
+  let coq_Zge = lazy (z_constant "Z.ge")
+  let coq_Zle = lazy (z_constant "Z.le")
+  let coq_Zlt = lazy (z_constant "Z.lt")
   let coq_Eq  = lazy (init_constant "eq")
 
-  let coq_Zplus = lazy (constant "Zplus")
-  let coq_Zminus = lazy (constant "Zminus")
-  let coq_Zopp = lazy (constant "Zopp")
-  let coq_Zmult = lazy (constant "Zmult")
-  let coq_Zpower = lazy (constant "Zpower")
+  let coq_Zplus = lazy (z_constant "Z.add")
+  let coq_Zminus = lazy (z_constant "Z.sub")
+  let coq_Zopp = lazy (z_constant "Z.opp")
+  let coq_Zmult = lazy (z_constant "Z.mul")
+  let coq_Zpower = lazy (z_constant "Z.pow")
 
   let coq_Qgt = lazy (constant "Qgt")
   let coq_Qge = lazy (constant "Qge")
-- 
cgit v1.2.3