diff options
| author | Erik Martin-Dorel | 2018-06-01 15:37:17 +0200 |
|---|---|---|
| committer | Erik Martin-Dorel | 2019-04-23 12:54:42 +0200 |
| commit | 2fed7b9a1870c7b921255ec055f0511ef530749d (patch) | |
| tree | 31e2ee07636429a06bda511f909f9c1c6227433b /doc/plugin_tutorial/tuto3/src | |
| parent | 964779322e0358dc821b03a67b4a7dd0b3b6d11e (diff) | |
[ssr] Define both a lemma "over" (in sig UNDER) and an ltac "over"
Both can be use to close the "under goals", in rewrite style or in
closing-tactic style.
Contrarily to the previous implementation that assumed
"over : forall (T : Type) (x : T), @Under T x x <-> True"
this new design won't require the Setoid library.
Extend the test-suite (in test-suite/ssr/under.v)
Diffstat (limited to 'doc/plugin_tutorial/tuto3/src')
0 files changed, 0 insertions, 0 deletions