Mercurial > cpdt > repo
changeset 298:123f466faedc
Small tweak to keep things working in 8.2
| author | Adam Chlipala <adam@chlipala.net> |
|---|---|
| date | Fri, 14 Jan 2011 14:55:32 -0500 |
| parents | b441010125d4 |
| children | 20c742997dae |
| files | src/Equality.v src/StackMachine.v |
| diffstat | 2 files changed, 10 insertions(+), 4 deletions(-) [+] |
line wrap: on
line diff
--- a/src/Equality.v Fri Jan 14 14:39:12 2011 -0500 +++ b/src/Equality.v Fri Jan 14 14:55:32 2011 -0500 @@ -156,10 +156,15 @@ Theorem get_imap : forall ls (mem : fmember elm ls) (hls : fhlist B ls), fhget (fhmap hls) mem = f (fhget hls mem). -(* begin thide *) +(* begin hide *) + induction ls; crush; case a0; reflexivity. +(* end hide *) + (** [[ induction ls; crush. + + ]] - (** In Coq 8.2, one subgoal remains at this point. Coq 8.3 has added some tactic improvements that enable [crush] to complete all of both inductive cases. To introduce the basics of reasoning about equality, it will be useful to review what was necessary in Coq 8.2 + In Coq 8.2, one subgoal remains at this point. Coq 8.3 has added some tactic improvements that enable [crush] to complete all of both inductive cases. To introduce the basics of reasoning about equality, it will be useful to review what was necessary in Coq 8.2. Part of our single remaining subgoal is: @@ -213,6 +218,7 @@ reflexivity. ]] *) + Qed. (* end thide *)
--- a/src/StackMachine.v Fri Jan 14 14:39:12 2011 -0500 +++ b/src/StackMachine.v Fri Jan 14 14:55:32 2011 -0500 @@ -1,4 +1,4 @@ -(* Copyright (c) 2008-2010, Adam Chlipala +(* Copyright (c) 2008-2011, Adam Chlipala * * This work is licensed under a * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0 @@ -21,7 +21,7 @@ (** I will start off by jumping right in to a fully-worked set of examples, building certified compilers from increasingly complicated source languages to stack machines. We will meet a few useful tactics and see how they can be used in manual proofs, and we will also see how easily these proofs can be automated instead. This chapter is not meant to give full explanations of the features that are employed. Rather, it is meant more as an advertisement of what is possible. Later chapters will introduce all of the concepts in bottom-up fashion. -I assume that you have installed Coq and Proof General. The code in this book is tested with Coq version 8.2pl2, though parts may work with other versions. +I assume that you have installed Coq and Proof General. The code in this book is tested with Coq versions 8.2pl2 and 8.3pl1, though parts may work with other versions. To set up your Proof General environment to process the source to this chapter, a few simple steps are required.