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