# HG changeset patch # User Adam Chlipala # Date 1379626112 14400 # Node ID a4b3386ae140b29aea4e31dfe7373e2ca055a644 # Parent 6b3fb6672cfa078b5ba4d7f64129c22dfa908dc5 Get StackMachine template generated properly again diff -r 6b3fb6672cfa -r a4b3386ae140 src/StackMachine.v --- a/src/StackMachine.v Sun May 12 12:50:27 2013 -0400 +++ b/src/StackMachine.v Thu Sep 19 17:28:32 2013 -0400 @@ -17,6 +17,12 @@ Require Import Bool Arith List CpdtTactics. Set Implicit Arguments. +(* begin hide *) +(* begin thide *) +Definition bleh := app_assoc. +(* end thide *) +(* end hide *) + (** In general, similar commands will be hidden in the book rendering of each chapter's source code, so you will need to insert them in from-scratch replayings of the code that is presented. To be more specific, every chapter begins with the above two lines, with the import list tweaked as appropriate, considering which definitions the chapter uses. The second command above affects the default behavior of definitions regarding type inference. *) @@ -401,12 +407,6 @@ If we did not already know the name of the theorem, we could use the %\index{Vernacular commands!SearchRewrite}%[SearchRewrite] command to find it, based on a pattern that we would like to rewrite: *) -(* begin hide *) -(* begin thide *) -Definition bleh := app_assoc. -(* end thide *) -(* end hide *) - SearchRewrite ((_ ++ _) ++ _). (** %\vspace{-.15in}%[[ app_assoc_reverse: