diff options
| author | Erik Martin-Dorel | 2019-03-01 16:06:14 +0100 |
|---|---|---|
| committer | Erik Martin-Dorel | 2019-04-23 12:54:43 +0200 |
| commit | 01b5e6e64b2af828b18fa6ee7037a7b7055f026e (patch) | |
| tree | 6029fc25ce24811dd3314b7ea0127731ae3a081b /test-suite | |
| parent | f294fe1684e03f63871864def0f82190da087ebe (diff) | |
[ssr] Remove the unify_helper tactic that appears unnecessary
It was only required in the (not realistic) test case "test_over_2_2",
which happened to introduce evars after the context variables.
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/ssr/over.v | 23 |
1 files changed, 12 insertions, 11 deletions
diff --git a/test-suite/ssr/over.v b/test-suite/ssr/over.v index 3bb5c03e08..cd6b196eeb 100644 --- a/test-suite/ssr/over.v +++ b/test-suite/ssr/over.v @@ -4,10 +4,11 @@ Axiom daemon : False. Ltac myadmit := case: daemon. (** Testing over for the 1-var case *) -Lemma test_over_1_1 : forall i : nat, False. +Lemma test_over_1_1 : False. intros. evar (I : Type); evar (R : Type); evar (x2 : I -> R). -assert (H : i + 2 * i - i = x2 i). +assert (H : forall i : nat, i + 2 * i - i = x2 i). + intros i. unfold x2 in *; clear x2; unfold R in *; clear R; unfold I in *; clear I. @@ -18,10 +19,11 @@ assert (H : i + 2 * i - i = x2 i). myadmit. Qed. -Lemma test_over_1_2 : forall i : nat, False. +Lemma test_over_1_2 : False. intros. evar (I : Type); evar (R : Type); evar (x2 : I -> R). -assert (H : i + 2 * i - i = x2 i). +assert (H : forall i : nat, i + 2 * i - i = x2 i). + intros i. unfold x2 in *; clear x2; unfold R in *; clear R; unfold I in *; clear I. @@ -34,10 +36,11 @@ Qed. (** Testing over for the 2-var case *) -Lemma test_over_2_1 : forall i j : nat, False. +Lemma test_over_2_1 : False. intros. evar (I : Type); evar (J : Type); evar (R : Type); evar (x2 : I -> J -> R). -assert (H : i + 2 * j - i = x2 i j). +assert (H : forall i j, i + 2 * j - i = x2 i j). + intros i j. unfold x2 in *; clear x2; unfold R in *; clear R; unfold J in *; clear J; @@ -49,10 +52,11 @@ assert (H : i + 2 * j - i = x2 i j). myadmit. Qed. -Lemma test_over_2_2 : forall i j : nat, False. +Lemma test_over_2_2 : False. intros. evar (I : Type); evar (J : Type); evar (R : Type); evar (x2 : I -> J -> R). -assert (H : i + 2 * j - i = x2 i j). +assert (H : forall i j : nat, i + 2 * j - i = x2 i j). + intros i j. unfold x2 in *; clear x2; unfold R in *; clear R; unfold J in *; clear J; @@ -61,9 +65,6 @@ assert (H : i + 2 * j - i = x2 i j). Fail done. rewrite over. - Fail done. (* Bug: doesn't work so we have to make a beta-expansion by hand *) - rewrite -[i + 2 * j - i]/((fun x y => x + 2 * y - x) i j). - (* cf. [plugins/ssr/ssreflect.v:unify_helper] *) done. myadmit. Qed. |