From 7da3e3d85c88eb42e932230048cb0db255474b5d Mon Sep 17 00:00:00 2001
From: fbesson <fbesson@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Fri, 20 May 2011 17:01:54 +0000
Subject: added support to handle division by a constant over R

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

(limited to 'plugins/micromega/Psatz.v')

diff --git a/plugins/micromega/Psatz.v b/plugins/micromega/Psatz.v
index 84ce85f29..325cc31bb 100644
--- a/plugins/micromega/Psatz.v
+++ b/plugins/micromega/Psatz.v
@@ -66,6 +66,7 @@ Ltac psatzl dom :=
         change (Tauto.eval_f (Qeval_formula (@find Q 0%Q __varmap)) __ff) ;
         apply (QTautoChecker_sound __ff __wit); vm_compute ; reflexivity)
   | R =>
+    unfold Rdiv in * ; 
     psatzl_R ;
     (* If csdp is not installed, the previous step might not produce any
     progress: the rest of the tactical will then fail. Hence the 'try'. *)
-- 
cgit v1.2.3