diff options
author | 2017-06-12 11:34:53 +0200 | |
---|---|---|
committer | 2017-10-05 23:30:05 +0200 | |
commit | 87a63ffc6dd36be0ef2e757b46f3c81f67f96207 (patch) | |
tree | ef900a9277584b91e436eaebecdef31779fc58f4 /Makefile.doc | |
parent | 2aac4ae818fec0d409da31ef9da83796d871d687 (diff) |
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.
Diffstat (limited to 'Makefile.doc')
0 files changed, 0 insertions, 0 deletions