From 300f78191ee00f86b22ffc6ab589fc0731dcfc6b Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Sun, 26 Apr 2020 14:30:18 -0400 Subject: [PATCH] Revising before class --- ProgramDerivation.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/ProgramDerivation.v b/ProgramDerivation.v index 135abfa..7422dad 100644 --- a/ProgramDerivation.v +++ b/ProgramDerivation.v @@ -497,7 +497,7 @@ Proof. simplify; subst; eauto. Qed. -Hint Resolve ReplaceMethod_ok. +Hint Resolve ReplaceMethod_ok : core. (* It is OK to replace a method body if the new refines the old as a [comp]. *) Theorem refine_method : forall state name (oldbody newbody : state -> nat -> comp (state * nat))