diff options
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. |