diff options
| author | Erik Martin-Dorel | 2019-10-31 22:08:47 +0100 |
|---|---|---|
| committer | Erik Martin-Dorel | 2019-10-31 22:15:46 +0100 |
| commit | 1090b272772c70a79fb082713451a935737cb1d3 (patch) | |
| tree | 71f11339350228222917a8fc1c95c9c59fd3d092 /test-suite | |
| parent | 2845bc2712604a3fab3b3a8497bb29b38acf2777 (diff) | |
[ssr] Refactor/Simplify the implementation of under
* Preserve the same behavior/interface but merge the two Module Types
(UNDER_EQ and) UNDER_REL.
* Remove the "Reflexive" argument in Under_rel.Under_rel
* Update plugin code (ssrfwd.ml) & Factor-out the main step
* Update the Hint (viz. apply over_rel_done => apply: over_rel_done)
* All the tests still pass!
Credits to @CohenCyril for suggesting this enhancement
Diffstat (limited to 'test-suite')
| -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 8232741b0d..267d981d05 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_eq_from_eq. + apply Under_rel_from_rel. 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_eq_from_eq. + apply Under_rel_from_rel. 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_eq_from_eq. + apply Under_rel_from_rel. 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_eq_from_eq. + apply Under_rel_from_rel. Fail done. rewrite over. |