From c6cc13587ce95e4d1e24fc8d4d864e4db3698abb Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Sat, 18 Nov 2017 12:15:15 -0500 Subject: [PATCH] Working again with Coq 8.6.1 --- CompilerCorrectness.v | 2 +- CompilerCorrectness_template.v | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/CompilerCorrectness.v b/CompilerCorrectness.v index d0b3b45..71c03c9 100644 --- a/CompilerCorrectness.v +++ b/CompilerCorrectness.v @@ -351,7 +351,7 @@ Proof. eapply plug_deterministic in H0; eauto. invert H0. match goal with - | [ H : step0 _ l' _ |- _ ] => eapply deterministic0 in H; eauto + | [ H : step0 _ _ _, H' : step0 _ _ _ |- _ ] => eapply deterministic0 in H; [ | apply H' ] end. propositional; subst; auto. invert H0. diff --git a/CompilerCorrectness_template.v b/CompilerCorrectness_template.v index 577f958..99e93fe 100644 --- a/CompilerCorrectness_template.v +++ b/CompilerCorrectness_template.v @@ -281,7 +281,7 @@ Proof. eapply plug_deterministic in H0; eauto. invert H0. match goal with - | [ H : step0 _ l' _ |- _ ] => eapply deterministic0 in H; eauto + | [ H : step0 _ _ _, H' : step0 _ _ _ |- _ ] => eapply deterministic0 in H; [ | apply H' ] end. propositional; subst; auto. invert H0.