Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
(Dis donc emacs, ceci est du -*-text-*- !)
LIST OF CHANGES
===============
version 1.05, 17/9/2003
=======================
o fixed pretty-printing of lambdas
o option -l also removes Load, Set/Unset Printing Coercions, Declare Step
version 1.04, 28/8/2003
=======================
o better spaces generated on source empty lines
o added tokens enclosed with square brackets [...] in (** printing
o hidden lemmas do not appear in index anymore
o HTML encoding &#xxx; now accepted in HTML escape sequences
o added syntax (** printing token $...Latex math...$ #...HTML...# *)
o option -l now suppresses Syntax, Grammar, Declare Morphism and Declare Step
o libraries do not appear anymore in HTML table of contents
o option -s suppresses titles in the table of contents
version 1.03, 17/7/2003
=======================
o new option -toc to get a table of contents (in toc.html with
-html, at the beginning of the document with -latex)
o fixed missing space on newline within comments
o new option -d to ouput files into a given directory
o fixed bug with -R
o only symbols containing balanced square brackets within [...]
version 1.0, 10/7/2003
======================
o new controls (** printing ... *) and (** remove printing ...*) to
customize idents/symbols pretty-printing
o fixed cleaning of temporary files when exiting abnormally
o new keywords: Notation, Declare Module
o cross references of Module (Type); distinction between modules and
libraries (.vo files)
o option -l also removes Section/Variable(s)/Hypothesis/End
version 0.7, 12/05/2003
=======================
o language support: options -latin1 and -utf8 (default behavior is
to assume ASCII 7 bits); options -inputenc and -charset for manual setting
o option --texmacs to translate to TeXmacs format, to be used by tmcoq
(see http://www-sop.inria.fr/lemme/Philippe.Audebaud/tmcoq/)
o environments (* begin show *) ... (* end show *) to show source,
whatever options are
o environment (* begin hide *) ... (* end hide *) to hide source,
whatever options are
o new option -l/--light for a light document without tactic
definitions, Require, Hint, etc. (see the manual)
o fixed gallina bug (-g) with "Local"
o LaTeX escape sequences no more printed in HTML documents
version 0.6, 15/11/2002
=======================
o compatibility with DOS files
o './' suppressed in front of filenames when turned into Coq module names
o interpretation of Coq's Comments (to be used with Pcoq)
version 0.5, 6/9/2002
=====================
o commands now interpreted within section titles
o new keywords: Module, Module Type, Import
o fixed bug in option -g (identifiers containing Coq keywords)
version 0.4, 5/4/2002
=====================
o fixed symbol pretty-print (e.g. A->~~A)
o closing comments with many stars allowed
version 0.3, 15/3/2002
======================
o fixed bug with -ps option
o links to Coq standard library (see options --no-externals / --coqlib)
version 0.2, 19/02/2002
=======================
o style.css mentioned in documentation and INSTALL and added to the tarballs
o added link to coqdoc homepage one page bottom, and missing