From 420f78b2caeaaddc6fe484565b2d0e49c66888e5 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Sun, 27 Jul 2014 10:02:38 +0200
Subject: Imported Upstream version 8.4pl4dfsg

---
 plugins/micromega/coq_micromega.ml | 34 +++++++++++++++++++---------------
 1 file changed, 19 insertions(+), 15 deletions(-)

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

diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index ff08aeb3..7e10464a 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-2012     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -275,10 +275,10 @@ struct
     *)
 
   let logic_dir = ["Coq";"Logic";"Decidable"]
-  let coq_modules =
-   init_modules @
-    [logic_dir] @ arith_modules @ zarith_base_modules @
-    [ ["Coq";"Lists";"List"];
+
+  let mic_modules = 
+    [ 
+      ["Coq";"Lists";"List"];
       ["ZMicromega"];
       ["Tauto"];
       ["RingMicromega"];
@@ -293,6 +293,10 @@ struct
       ["Coq";"Reals" ; "Rpow_def"];
       ["LRing_normalise"]]
 
+  let coq_modules =
+   init_modules @
+    [logic_dir] @ arith_modules @ zarith_base_modules @ mic_modules
+
   let bin_module = [["Coq";"Numbers";"BinNums"]]
 
   let r_modules =
@@ -312,7 +316,7 @@ struct
   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 m_constant = gen_constant_in_modules "ZMicromega" mic_modules
 
   let coq_and = lazy (init_constant "and")
   let coq_or = lazy (init_constant "or")
@@ -354,15 +358,15 @@ struct
   let coq_Qmake = lazy (constant "Qmake")
 
   let coq_Rcst = lazy (constant "Rcst")
-  let coq_C0   = lazy (constant "C0")
-  let coq_C1   = lazy (constant "C1")
-  let coq_CQ   = lazy (constant "CQ")
-  let coq_CZ   = lazy (constant "CZ")
-  let coq_CPlus = lazy (constant "CPlus")
-  let coq_CMinus = lazy (constant "CMinus")
-  let coq_CMult  = lazy (constant "CMult")
-  let coq_CInv   = lazy (constant "CInv")
-  let coq_COpp   = lazy (constant "COpp")
+  let coq_C0   = lazy (m_constant "C0")
+  let coq_C1   = lazy (m_constant "C1")
+  let coq_CQ   = lazy (m_constant "CQ")
+  let coq_CZ   = lazy (m_constant "CZ")
+  let coq_CPlus = lazy (m_constant "CPlus")
+  let coq_CMinus = lazy (m_constant "CMinus")
+  let coq_CMult  = lazy (m_constant "CMult")
+  let coq_CInv   = lazy (m_constant "CInv")
+  let coq_COpp   = lazy (m_constant "COpp")
 
 
   let coq_R0    = lazy (constant "R0")
-- 
cgit v1.2.3