diff options
| author |  Pierre Letouzey <pierre.letouzey@inria.fr> | 2017-06-12 11:34:53 +0200 |
|---|---|---|
| committer | Pierre Letouzey <pierre.letouzey@inria.fr> | 2017-10-05 23:30:05 +0200 |
| commit | 87a63ffc6dd36be0ef2e757b46f3c81f67f96207 (patch) | |
| tree | ef900a9277584b91e436eaebecdef31779fc58f4 /CHANGES | |
| 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 'CHANGES')
| -rw-r--r-- | CHANGES | 3 |
1 files changed, 3 insertions, 0 deletions
@@ -12,6 +12,9 @@ Tactics utility. The command "Set NativeCompute Profiling" enables profiling, and "Set NativeCompute Profile Filename" customizes the profile filename. +- The tactic "omega" is now aware of the bodies of context variables + such as "x := 5 : Z" (see bug #148). This could be disabled via + Unset Omega UseLocalDefs. Changes from 8.7+beta1 to 8.7.0 =============================== |