Added NIso.v to Makefile.common. Changed Examples.v in contrib/micromega to use NRing instead of Ring_polynom.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10264 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 22 insertions, 7 deletions

diff --git a/Makefile.common b/Makefile.common
index 004cef640..ccc5d94cd 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -672,7 +672,8 @@ NATURALABSTRACTVO:=\
   $(NATABSTRACTDIR)/NTimes.vo\
   $(NATABSTRACTDIR)/NOrder.vo\
   $(NATABSTRACTDIR)/NTimesOrder.vo\
-  $(NATABSTRACTDIR)/NMinus.vo
+  $(NATABSTRACTDIR)/NMinus.vo\
+  $(NATABSTRACTDIR)/NIso.vo
 
 NATURALPEANOVO:=$(NATURALDIR)/Peano/NPeano.vo
 NATURALBINARYVO:=$(NATURALDIR)/Binary/NBinary.vo
diff --git a/contrib/micromega/Examples.v b/contrib/micromega/Examples.v
index 976815142..6bb9311a5 100644
--- a/contrib/micromega/Examples.v
+++ b/contrib/micromega/Examples.v
@@ -1,10 +1,15 @@
 Require Import OrderedRing.
 Require Import RingMicromega.
-Require Import Ring_polynom.
 Require Import ZCoeff.
 Require Import Refl.
 Require Import ZArith.
 Require Import List.
+(*****)
+Require Import NRing.
+Require Import VarMap.
+(*****)
+(*Require Import Ring_polynom.*)
+(*****)
 
 Import OrderedRingSyntax.
 
@@ -55,7 +60,11 @@ Lemma plus_minus : forall x y : R, x + y == 0 -> x - y == 0 -> x < 0 -> False.
 Proof.
 intros x y.
 Open Scope Z_scope.
-set (varmap := fun (x y : R) => x :: y :: nil).
+(*****)
+set (env := fun x y : R => Node (Leaf y) x (Empty _)).
+(*****)
+(*set (env := fun (x y : R) => x :: y :: nil).*)
+(*****)
 set (expr :=
  Build_Formula (PEadd (PEX Z 1) (PEX Z 2)) OpEq (PEc 0)
    :: Build_Formula (PEsub (PEX Z 1) (PEX Z 2)) OpEq (PEc 0)
@@ -63,7 +72,7 @@ set (expr :=
 set (cert :=
    S_Add (S_Mult (S_Pos 0 Zeq_bool Zle_bool 2 (refl_equal true)) (Z_In 2))
      (S_Add (S_Ideal (PEc 1) (Z_In 1)) (S_Ideal (PEc 1) (Z_In 0)))).
-change (make_impl (Zeval_formula (varmap x y)) expr False).
+change (make_impl (Zeval_formula (env x y)) expr False).
 apply (check_formulas_sound sor ZSORaddon expr cert).
 reflexivity.
 Close Scope Z_scope.
@@ -77,7 +86,11 @@ Lemma Zdiscr :
     a * (x * x) + b * x + c == 0 -> 0 <= b * b - four * a * c.
 Proof.
 Open Scope Z_scope.
-set (varmap := fun (a b c x : R) => a :: b :: c :: x:: nil).
+(*****)
+set (env := fun (a b c x : R) => Node (Node (Leaf x) b (Empty _)) a (Leaf c)).
+(*****)
+(*set (env := fun (a b c x : R) => a :: b :: c :: x:: nil).*)
+(*****)
 set (poly1 :=
      (Build_Formula
            (PEadd
@@ -93,10 +106,11 @@ set (wit :=
           (Z_Square
              (PEadd (PEmul (PEc 2) (PEmul (PEX Z 1) (PEX Z 4))) (PEX Z 2))))) :: nil).
 intros a b c x.
-change (make_impl (Zeval_formula (varmap a b c x)) poly1
-  (make_conj (Zeval_formula (varmap a b c x)) poly2)).
+change (make_impl (Zeval_formula (env a b c x)) poly1
+  (make_conj (Zeval_formula (env a b c x)) poly2)).
 apply (check_conj_formulas_sound sor ZSORaddon poly1 poly2 wit).
 reflexivity.
+Close Scope Z_scope.
 Qed.
 
 End Examples.