From e20e6b3b9e4148f62c94bfb467817feb2b6a4583 Mon Sep 17 00:00:00 2001
From: fbesson
Date: Wed, 29 Jun 2011 16:58:47 +0000
Subject: update of Micromega doc

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14248 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 plugins/micromega/Psatz.v | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'plugins')

diff --git a/plugins/micromega/Psatz.v b/plugins/micromega/Psatz.v
index 88d0332dcc..7f6cf79bec 100644
--- a/plugins/micromega/Psatz.v
+++ b/plugins/micromega/Psatz.v
@@ -81,12 +81,14 @@ Ltac lra :=
   first [ psatzl R | psatzl Q ].
 
 Ltac lia :=
+  zify ; unfold Zsucc in * ; 
   (*cbv delta - [Zplus Zminus Zopp Zmult Zpower Zgt Zge Zle Zlt iff not] ;*) xlia ; 
   intros __wit __varmap __ff ;
     change (Tauto.eval_f (Zeval_formula (@find Z Z0 __varmap)) __ff) ;
       apply (ZTautoChecker_sound __ff __wit); vm_compute ; reflexivity.
 
 Ltac nia :=
+  zify ; unfold Zsucc in * ; 
   xnlia ;
   intros __wit __varmap __ff ;
     change (Tauto.eval_f (Zeval_formula (@find Z Z0 __varmap)) __ff) ;
-- 
cgit v1.2.3