Coqdoc patches from UPenn (thanks to C. Casinghino). This introduces the

ability to format inference rules (delimited by [[[ ]]]) and adds some
new flags. Here's the message from Chris:

- coqdoc now has support for inference rules inside coqdoc comments.
 These should be enclosed in triple square brackets with the
 following format.

[[[
                      |- t1 : Bool
                 |- t2 : T    |- t3 : T
               ----------------------------                   (T_If)
               |- if t1 then t2 else t3 : T
]]]

 The rule's name is optional.  Multiple inference rules may be
 included in the same [[[ ]]] block, separated by blank lines.
 See http://www.cis.upenn.edu/~bcpierce/sf/Stlc.html#lab469
 for some examples of the output.  The output will only be pretty
 in html - in other formats it is printed verbatim (though it
 shouldn't be hard to add latex support, and I may soon).

- Two new coqdoc flags have been added.  First, --inline-notmono
 causes inline code to be printed in a proportional width font
 (adjustable in the css file).  Second, --no-glob tells coqdoc not to
 look for .glob files (no links will be inserted for identifiers when
 this flag is used).

- Finally, the handling of paragraphs and whitespace around lists
 has been made somewhat saner.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13473 85f007b7-540e-0410-9357-904b9bb8a0f7

0 files changed, 0 insertions, 0 deletions