Omega now aware of context variables with bodies (in type Z or nat) (fix bug 148)

 For compatibility, this extra feature of omega could be disabled via
  Unset Omega UseLocalDefs.

 Caveat : for now, real let-ins inside goals or hyps aren't handled, use
 some "cbv zeta" reduction if you want to get rid of them. And context
 definitions whose types aren't Z or nat are ignored, some manual "unfold"
 are still mandatory if expanding these definitions will help omega.

0 files changed, 0 insertions, 0 deletions