diff options
| author | Erik Martin-Dorel | 2019-04-03 15:03:02 +0200 |
|---|---|---|
| committer | Erik Martin-Dorel | 2019-04-23 20:22:38 +0200 |
| commit | 4bc91ba5654574d156ebf2934a6fb36d31b40ff9 (patch) | |
| tree | b07446667570d47d50478a7d40f304fe4d9617ee /test-suite/ssr | |
| parent | e1e5d40a0f351cbf01f7e66d049f9a937d5f8563 (diff) | |
[ssr] Define over as a rewrite rule & Merge 'Under[ _ ] notations
as suggested by @gares, and:
* Rename some Under_* terms for better uniformity;
* Update & Improve minor details in the documentation.
Diffstat (limited to 'test-suite/ssr')
| -rw-r--r-- | test-suite/ssr/over.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/test-suite/ssr/over.v b/test-suite/ssr/over.v index cd6b196eeb..8232741b0d 100644 --- a/test-suite/ssr/over.v +++ b/test-suite/ssr/over.v @@ -12,7 +12,7 @@ assert (H : forall i : nat, i + 2 * i - i = x2 i). unfold x2 in *; clear x2; unfold R in *; clear R; unfold I in *; clear I. - apply Under_from_eq. + apply Under_eq_from_eq. Fail done. over. @@ -27,7 +27,7 @@ assert (H : forall i : nat, i + 2 * i - i = x2 i). unfold x2 in *; clear x2; unfold R in *; clear R; unfold I in *; clear I. - apply Under_from_eq. + apply Under_eq_from_eq. Fail done. by rewrite over. @@ -45,7 +45,7 @@ assert (H : forall i j, i + 2 * j - i = x2 i j). unfold R in *; clear R; unfold J in *; clear J; unfold I in *; clear I. - apply Under_from_eq. + apply Under_eq_from_eq. Fail done. over. @@ -61,7 +61,7 @@ assert (H : forall i j : nat, i + 2 * j - i = x2 i j). unfold R in *; clear R; unfold J in *; clear J; unfold I in *; clear I. - apply Under_from_eq. + apply Under_eq_from_eq. Fail done. rewrite over. |