Skip to content

C
cpdt
Commit d74632eb authored by Adam Chlipala's avatar Adam Chlipala
Browse files
Options

Working again with Coq 8.4

parent 9e80cf97
Hide whitespace changes
Inline Side-by-side
Showing with 2 additions and 0 deletions
src/GeneralRec.v
View file @ d74632eb
...@@ -822,6 +822,7 @@ Lemma cassociativity1 : forall A B C (f : A -> comp B) (g : B -> comp C) r c, ...@@ -822,6 +822,7 @@ Lemma cassociativity1 : forall A B C (f : A -> comp B) (g : B -> comp C) r c,
match goal with match goal with
| [ H : Bnd _ _ = Bnd _ _ |- _ ] => injection H; clear H; intros; try subst | [ H : Bnd _ _ = Bnd _ _ |- _ ] => injection H; clear H; intros; try subst
end. end.
subst B.
crush. crush.
inversion H; clear H; crush. inversion H; clear H; crush.
eauto. eauto.
...@@ -835,6 +836,7 @@ Lemma cassociativity2 : forall A B C (f : A -> comp B) (g : B -> comp C) r c, ...@@ -835,6 +836,7 @@ Lemma cassociativity2 : forall A B C (f : A -> comp B) (g : B -> comp C) r c,
match goal with match goal with
| [ H : Bnd _ _ = Bnd _ _ |- _ ] => injection H; clear H; intros; try subst | [ H : Bnd _ _ = Bnd _ _ |- _ ] => injection H; clear H; intros; try subst
end. end.
subst A.
crush. crush.
inversion H0; clear H0; crush. inversion H0; clear H0; crush.
eauto. eauto.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment