diff options
author | 2015-10-28 12:42:27 +0100 | |
---|---|---|
committer | 2015-10-28 12:52:27 +0100 | |
commit | e3ec13976d39909ac6f1a82bf1b243ba8a895190 (patch) | |
tree | a3cc4d0611b153e2ffec235d58eef53861de5e10 /test-suite | |
parent | 38aacaa96abee65edb64bf88f15016d54ce31568 (diff) |
Revert "Fixing #4198 (continued): not matching within the inner lambdas/let-ins"
After all, let's target 8.6.
Diffstat (limited to 'test-suite')
-rw-r--r-- | test-suite/success/ltac.v | 26 |
1 files changed, 0 insertions, 26 deletions
diff --git a/test-suite/success/ltac.v b/test-suite/success/ltac.v index 5bef2e512..6c4d4ae98 100644 --- a/test-suite/success/ltac.v +++ b/test-suite/success/ltac.v @@ -317,29 +317,3 @@ let T := constr:(fun a b : nat => a) in end. exact (eq_refl n). Qed. - -(* Check that matching "match" does not look into the invisible - canonically generated binders of the return clause and of the branches *) - -Goal forall n, match n with 0 => true | S _ => false end = true. -intros. unfold nat_rect. -Fail match goal with |- context [nat] => idtac end. -Abort. - -(* Check that branches of automatically generated elimination - principle are correctly eta-expanded and hence matchable as seen - from the user point of view *) - -Goal forall a f n, nat_rect (fun _ => nat) a f n = 0. -intros. unfold nat_rect. -match goal with |- context [f _] => idtac end. -Abort. - -(* Check that branches of automatically generated elimination - principle are in correct form also in the presence of let-ins *) - -Inductive a (b:=0) : let b':=1 in Type := c : let d:=0 in a. -Goal forall x, match x with c => 0 end = 1. -intros. -match goal with |- context [0] => idtac end. -Abort. |