diff options
author | ckeller <ckeller@users.noreply.github.com> | 2021-04-26 16:25:57 +0200 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-04-26 16:25:57 +0200 |
commit | 1cd1e8d4e3399a582c2f5b8de203ba59cd3f8010 (patch) | |
tree | c5e7203ff4ac418a5d6206690bf13df2ef0f59a1 /src/lfsc/ast.mli | |
parent | f7ecc2f20d4cd8d777e6169675a4057148bf6ccb (diff) | |
download | smtcoq-1cd1e8d4e3399a582c2f5b8de203ba59cd3f8010.tar.gz smtcoq-1cd1e8d4e3399a582c2f5b8de203ba59cd3f8010.zip |
Take hypotheses from the local context (#91)
* The tactics sets veritXXX and smtXXX now automatically take hypotheses from the local context
* `prop2bool_hyps` also apply to hypotheses not in the local context
* Second strategy for vauto (still incomplete)
Diffstat (limited to 'src/lfsc/ast.mli')
0 files changed, 0 insertions, 0 deletions