tests are now handled with a standard Makefile that does not use do_tests.sh

another step roward the removal of do_tests.sh

removed php-shell scripts

moved to the new table

fix

fixed a bug in the Makefile, generatedGui.mli no more there

one more step toward release and bench reorganization

fix

more work for the release

snapshot for release

added elp to distribution

added check to not clean the standard library, a confirmation is required

Huge commit for the release. Includes:
- getter_storage modifications to honor multiple (overlapping)
  ro/rw repositories
- removes of ~basedir
- addition of the 'publish' matitamake command used to install in system
  tables/directory a development (that is compiling with -system)
- removal of .build,.user,.devel config files (only one is needed)
- fixed make dist/install to strip binaries, install the library with the new
  method
- fixed compilation of the getter daemon
- deletion of grafite misc that is no more needed

Added inversion principle creation for inductive predicates.

Inversion code cleaning.

use the statusbar to display hyperlink targets

Debugging code removed.

Reduction trick added to simplify (greatly speeding up some examples
in library/algebra. For instance, a simplification that used to be performed
in more than 4h now takes less than 1s).

The idea is simply to avoid delta-reduction of a constant applied to
arguments that are not "active" (i.e. they cannot create a redex when
substituted in the body of the constant).

hand-like cursor when the cursor is on an href in a clickable math view

- added an hack to load sequents viewer's mathml from file
- tried organizing entries of the debug menu

This simplify seems to diverge!

First theorems proved on left cosets.

added the creation of system_tables to the db when creating the user environment

PP of Refine.RefineFailure.

Use reference counting to keep track of camlp4 extensions so that the same
grammar rules are not added several times. (closes: #147)

added a generic (yet rather trivial) module for reference counting

bugfix: use utf8-aware substring function

added "gragrep", grep-like tool over a bunch of grafite scripts

added capability to specify externally extra command line arguments so that we
are no longer constrained to have all command line tools share the same command
line interface

Added module GrafiteWalker, which implements traversals (recursive and not) over
grafite scripts. Useful for grep/sed like operations over a bunch of scripts.

factorized an ast_statement type which is (now) used from outside this module

- added src_root build time configuration value
- added the disclaimer "ComponentsConf should not be here"

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.