diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-12-22 19:45:04 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-10-26 15:34:50 +0200 |
| commit | 91e9e1c26b7f2b874df83600b2bc8d23df9ed48b (patch) | |
| tree | 770c08abffe9c2ea689cfa0f2e49cf9da445888c /CHANGES | |
| parent | 925c434592597a34cd7ef4efb5e18a43e197bd96 (diff) | |
Passing around the flag for injection so that tactics calling inj at
ML level can set the flags themselves.
In particular, using injection and discriminate with option "Keep
Proofs Equalities" when called from "decide equality" and "Scheme
Equality".
This fixes bug #5281.
Diffstat (limited to 'CHANGES')
| -rw-r--r-- | CHANGES | 2 |
1 files changed, 2 insertions, 0 deletions
@@ -18,6 +18,8 @@ Tactics such as "x := 5 : Z" (see BZ#148). This could be disabled via Unset Omega UseLocalDefs. - The tactic "romega" is also aware now of the bodies of context variables. +- Tactic "decide equality" now able to manage constructors which + contain proofs. Changes from 8.7+beta2 to 8.7.0 =============================== |