information on current compilation state added in each file

64 "change" here and there in the library are now simplify/unfold as they
should have been. This has been possible because of some bugs fixed.

During simplify, reduction of the argument of a Fix and of a MutCase is now
performed using simplify. (It used to be performed by whd).
Pros: sometimes you should get simpler terms (but not so far)
Cons: sometimes simplification could simplify less than expected (but not so far)

improved comment of HExtlib.find

- ensure simplify_deps exists when invoked
- added a SIMPLIFYDEPS variable to change its location

moved initial (i.e. empty) lexiconEngine status to lexiconEngine from
lexiconSync

simplify used in place of change

Bug fixed in simplify: delta expansion of constants applied to more arguments
than head lambda abstractions was always performed (even if no "interesting"
reduction took place).

changed structure of the generated utf8MacroTable.ml file so that it can be
compiled with ocamlopt avoiding Stack_overflow

Missing -I ../.. added.

First part of bug #152 (unable to exit from Matita) solved.

Order of compilation of the modules fixed.

Coercions are now hidden by default in termAcicContent.ml.

Coercions are now hidden by default (in termAcicContent.ml)

pack_coercion used to avoid packing n-ary coercions where n > 2.
Fixed.

Stupid bug fixed.

Packing of implicit coercions must be also performed as soon as an object (or proof status) is created.

Finished one lemma (after many bug fixes here and there).

Bug fixed: rewrite > t where t had occurrences of metavariables in it could
fail because of a missing apply_subst.

Localization bug fixed.

Some more implicit coercions here and there.

Bug fixed in pack_coercions_obj. The context of the metas in the metasenv of
the CurrentProof was not translated correctly.

class definition updated (but buggy now)

Bug fixed: the source and target of declared parametric coercions used to
be URIs of the inductive block instead of being URIs of single inductive
types or constructors.

Trivial bug fixed in the merging of polymorphic coercions.

Bug fixed in insertion of parametric coercions.
To fix the bug, the CoercGraph.look_for_coercion now returns a term saturated
with Cic.Implicits. As usual, remember to refine the term before further usage.

More refinement errors localized.

More refinement errors localized.

Bug fixed: the wrong exception was enriched, breaking the invariant that
only unlocalized exceptions can be enriched.

Sys.command -> Unix.system

tentative speedup not coercion-packing the proof after every step

added support for "polymorphic" coercions

fix

fix

fix

fix

added info on how to create the dumps

added snapshot of the coq exportation metadata

tentative fix

reverted orrible but correct syntax

fixed syntax

Recapitalization of sect_tactics.xml

Some fixes in the documentation of the tactics.

A few intros_spec were missing here and there.

Typo fixed.

Most of the tactics are now documented.

completed installation instructions

Even more tactics documented.

New tactics (badly) documented.

implemented "install" target

build temporary library in software/matita/.matita (instead of software/.matita)

removed duplicate copy of AUTHORS

install in /usr/local/matita/

expand SRCROOT (is needed by matita/Makefile)

bumped year

Nicer index for tactics in Yelp.

ported to the docbook "book"

Strange fix (for a yelp bug?)

From article to book

comment out an incomplete proof

More tactics documented.

Several more tactics documented.

Never implemented tactics compare and decide equality purged from the code.

added title to sliced htmls

added pretty printing of generated xml files via xmllint --format

added generation of .html and .txt version of manual parts

- removed old commented code
- added copyright notice

Help for the first two tactics.

added splitting engine for .html generated by docbook -> xhtml conversion

no more dummy names for building the library in distributed tarballs

"sec_" prefix for section IDs

Added a few basic definitions of subgroups and left cosets (together with
their extreme notation!)

added instructions (some gaps still to be filled in, notably: ./configure
parameters and instructions on how to create the mysql database)

written install section up to build requirements

changed location of version.txt

added dir for released matita tarballs

- moved version.txt.in to the help dir
- added Makefile to generate xhtml and pdf from the docbook manual

reshaped manual

- use the best matitamake to build the library on dist
- renamed dist targets so that they are distinguishable and not callable in
  when developing matita

fill DISTRIBUTED value on dist

removed useless grepping -v

- factorization of the recursive rule
- added "library" target to build the stdlib when distributed
- implemented "distcheck" target

added configure time values SRCROOT and DISTRIBUTED

factorization of the recursive rule

added Matitamake interface

added last-modified info at the bottom of every page

- escaped "&" in URLs so that all pages are now XHTML 1.0 Strict valid
- expanded a bit the "nothing to see here" concept in the matita web pages

removed papers dir, now all papers are in the new "papers" repository

removed papers that have been moved to the new "papers" repository

absolute path and factorization for matita.basedir

- changed semantics of "init": now it is idempotent
- added support for "-v" flag printing "make" command line
- minor change: lazy discovering of whether we are ".opt" or not

use matita.verbosity instead of matita.quiet

- uniformed command line handling of matitamake with that of other matita tools
- changed "-q" flag semantics: now it reduce the "matita.verbosity" value by 1
  unit
- added "-v" flag: it increase the "matita.verbosity" value by 1
- "matita.quiet" is no longer in use

help path is no longer hard coded but relative to runtime base dir

fixed tactic ids to include a "tac_" prefix

- bugfix: pass -conffile to matitamake
- more quiet feedback during compilation of stdlib

Basic facts about group morphisms.

moved mathql/ under software/

first sketch of the documentation (to be used by yelp)

s/ocaml/components/ in the "tag" target