diff options
author | 2016-12-22 19:45:04 +0100 | |
---|---|---|
committer | 2017-10-26 15:34:50 +0200 | |
commit | 91e9e1c26b7f2b874df83600b2bc8d23df9ed48b (patch) | |
tree | 770c08abffe9c2ea689cfa0f2e49cf9da445888c /lib/hook.ml | |
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 'lib/hook.ml')
0 files changed, 0 insertions, 0 deletions