diff options
| author | Erik Martin-Dorel | 2018-05-29 23:07:02 +0200 |
|---|---|---|
| committer | Erik Martin-Dorel | 2019-04-02 20:25:00 +0200 |
| commit | bf4fdaa1836a17e4d36d38ba47959d1f50155a7b (patch) | |
| tree | 6f7270e1d61eaa47615f0cf738cc1bb6e9784947 /doc/plugin_tutorial/tuto3 | |
| parent | 424c1973e96dfbf3b2e3245d735853ffa9600373 (diff) | |
[ssr] under: rewrite takes an optional bool arg
* If this flag under=true: enable flag with_evars of refine_with
to create evar(s) if the "under lemma" has non-inferable args.
* Backward compatibility of ssr rewrite is kept.
* Fix test-suite/ssr/dependent_type_err.v
Diffstat (limited to 'doc/plugin_tutorial/tuto3')
0 files changed, 0 insertions, 0 deletions