Mercurial > cpdt > repo
comparison src/Extensional.v @ 204:cbf2f74a5130
Parts I want to keep compile with 8.2
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Fri, 06 Nov 2009 10:52:43 -0500 |
parents | df289eb8ef76 |
children | d1464997078d |
comparison
equal
deleted
inserted
replaced
203:71ade09024ac | 204:cbf2f74a5130 |
---|---|
961 generalize (elaboratePat_correct P S F V); intros; | 961 generalize (elaboratePat_correct P S F V); intros; |
962 destruct (patDenote P V); try discriminate | 962 destruct (patDenote P V); try discriminate |
963 | [ H : forall env, Some _ = Some env -> _ |- _ ] => | 963 | [ H : forall env, Some _ = Some env -> _ |- _ ] => |
964 destruct (H _ (refl_equal _)); clear H; intuition | 964 destruct (H _ (refl_equal _)); clear H; intuition |
965 | [ H : _ |- _ ] => rewrite H; intuition | 965 | [ H : _ |- _ ] => rewrite H; intuition |
966 | [ |- context[match ?v with inl _ => _ | inr _ => _ end] ] => destruct v; auto | |
966 end. | 967 end. |
967 Qed. | 968 Qed. |
968 | 969 |
969 Implicit Arguments letify [var t ts]. | 970 Implicit Arguments letify [var t ts]. |
970 | 971 |