Mercurial > cpdt > repo

diff src/Subset.v @ 439:393b8ed99c2f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
A pass of improvements to vertical spacing, up through end of InductiveTypes
author Adam Chlipala <adam@chlipala.net>
date Mon, 30 Jul 2012 13:21:36 -0400
parents 8077352044b2
children f923024bd284
line wrap: on
line diff
--- a/src/Subset.v	Fri Jul 27 16:55:30 2012 -0400
+++ b/src/Subset.v	Mon Jul 30 13:21:36 2012 -0400
@@ -258,16 +258,16 @@
 
      We do most of the work with the %\index{tactics!refine}%[refine] tactic, to which we pass a partial "proof" of the type we are trying to prove.  There may be some pieces left to fill in, indicated by underscores.  Any underscore that Coq cannot reconstruct with type inference is added as a proof subgoal.  In this case, we have two subgoals:
 
-%\vspace{.1in} \noindent 2 \coqdockw{subgoals}\vspace{-.1in}%#<tt>2 subgoals</tt>#
 [[
+2 subgoals
   
   n : nat
   _ : 0 > 0
   ============================
    False
-]]
-%\noindent \coqdockw{subgoal} 2 \coqdockw{is}:%#<tt>subgoal 2 is</tt>#
-[[
+
+subgoal 2 is
+
  S n' = S n'
  ]]