diff options
author | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-10-17 17:26:38 +0200 |
---|---|---|
committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-10-18 20:11:14 +0200 |
commit | 8748947349a206a502e43cfe70e3397ee457c4f7 (patch) | |
tree | e1fb17ec7aee812b7ca462c8c644d0155ae88d44 /test-suite/success/ltac.v | |
parent | 23545b802a14b2fad10f4382604c71f55b7d6d0e (diff) |
Fixing #4198 (continued): not matching within the inner lambdas/let-ins
of the return clause and of the branches (what assumed that the
implementation preserves the invariant that the return predicate and
the branches are in canonical [fun Δ => t] form, with Δ possibly
containing let-ins).
Diffstat (limited to 'test-suite/success/ltac.v')
-rw-r--r-- | test-suite/success/ltac.v | 26 |
1 files changed, 26 insertions, 0 deletions
diff --git a/test-suite/success/ltac.v b/test-suite/success/ltac.v index 6c4d4ae98..5bef2e512 100644 --- a/test-suite/success/ltac.v +++ b/test-suite/success/ltac.v @@ -317,3 +317,29 @@ 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. |