From 95c80b62371bf66da847a5a42b7e8ca2bcef12b5 Mon Sep 17 00:00:00 2001
From: fbesson
Date: Wed, 18 May 2011 20:55:10 +0000
Subject: apply zeta reduction before syntaxification

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14139 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 plugins/micromega/coq_micromega.ml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'plugins')

diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index 687d24ac7b..ebf44e74c7 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -988,7 +988,7 @@ struct
     * This is the big generic function for formula parsers.
     *)
   
-  let parse_formula parse_atom env term =
+  let parse_formula parse_atom env tg term =
 
     let parse_atom env tg t = try let (at,env) = parse_atom env t in
                                     (A(at,tg,t), env,Tag.next tg) with _ -> (X(t),env,tg) in
@@ -1019,7 +1019,7 @@ struct
       | _ when term = Lazy.force coq_True -> (TT,env,tg)
       | _ when term = Lazy.force coq_False -> (FF,env,tg)
       | _  -> X(term),env,tg in
-    xparse_formula env term
+    xparse_formula env tg  (Reductionops.whd_zeta term)
 
   let dump_formula typ dump_atom f =
    let rec xdump f =
@@ -1808,13 +1808,13 @@ let xlia gl =
   try 
     micromega_gen parse_zarith Mc.negate Mc.normalise Mc.runsat Mc.rdeduce zz_domain_spec
       [ linear_Z ] gl
-  with z -> Printexc.print_backtrace stdout ; raise z
+  with z -> (*Printexc.print_backtrace stdout ;*) raise z
 
 let xnlia gl =
   try 
     micromega_gen parse_zarith Mc.negate Mc.normalise Mc.runsat Mc.rdeduce zz_domain_spec
       [ nlinear_Z ] gl
-  with z -> Printexc.print_backtrace stdout ; raise z
+  with z -> (*Printexc.print_backtrace stdout ;*) raise z
 
 
 
-- 
cgit v1.2.3