| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2019-04-23 | [ssr] set under's tactic argument at LEVEL 3 | Erik Martin-Dorel | |
| So if the underlying tactic "contains a ;" one should actually write: under eq_bigl => i do [rewrite andb_idl; first by move/eqP->]. | |||
| 2019-04-23 | [ssr] Define over as a rewrite rule & Merge 'Under[ _ ] notations | Erik Martin-Dorel | |
| as suggested by @gares, and: * Rename some Under_* terms for better uniformity; * Update & Improve minor details in the documentation. | |||
| 2019-04-23 | [ssr] Add small output test for "under eq_G => m do rewrite subnn" | Erik Martin-Dorel | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |