diff options
| author | fbesson | 2011-05-18 20:55:10 +0000 |
|---|---|---|
| committer | fbesson | 2011-05-18 20:55:10 +0000 |
| commit | 95c80b62371bf66da847a5a42b7e8ca2bcef12b5 (patch) | |
| tree | 743f32ac6d447d271db9228e9290ac7264a5e9c8 | |
| parent | 26d91f7947d45d0c125cebee58ac8dd0a6bb6ac3 (diff) | |
apply zeta reduction before syntaxification
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14139 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | plugins/micromega/coq_micromega.ml | 8 |
1 files changed, 4 insertions, 4 deletions
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 |