Bug fixed: terms with a Cast used to raise assert false when whd was avoided
by the conversion strategy.

Huge speed-up in conversion: the old conversion strategy is set back.
 1. try to "convert" the two terms recursively without performing reduction
 2. if it fails, do a whd and try again
The overall result on the library of Coq is really remarkable.

#### EXPERIMENTAL COMMIT ####
Added a potentially dangerous ~expand_beta_redexes flag to
CicSubstitution.subst. If used carefully, it enormously speeds up
the type-checking of many theorems (since a very frequent conversion test
happens between a beta-redex and its contractum).

Debugging code added.

removed unif_ty ref

reverted the addition of _ to mistyped names

few bits to debug the benchmark system

deals with colors

more profiling and fixes for paramod

args removed from equalities.
New selection strategy. De morgan: 253 s.

Debugging code commented out.

* trust = true
* better pretty-printing of type-checking exceptions

"Performance bug" fixed: I removed a whd in the does_not_occur function.
Consequences:
  1. incredible speed-up in the type-checking of certain inductive types
  2. "dummy" occurrences (i.e. occurrences that are doomed to disappear because
     of reduction) are now rejected (they used to be accepted). Coq has the
     same behaviour.

Several "try ... with _ -> " specialized.

More robust handling of Control-C.

Flush stdout added in proper position.

ignoring test_library{,.opt}

Recently introduced bug fixed in the kernel: a stack was "forgot" during
reduction of a MutCase.

Unable to parse my own output. Fixed.

% forgot in the output

Serious test for the Coq library added (name test_library).
Input: a file that holds a list of URIs.
Output: the benchmark; the output file is also a valid input.
        In this case the output also prints the differences w.r.t. the
        last execution.
Ctrl-break can be used to interrupt the type-checking of a single URI.
An interactive question is posed to the user to decide if proceeding with
the next URIs or not.

more error messages were on stdout :-(

error message was printed on stdout

Colors are back! :-)

New unification and new matching.

Legend for profiling printed iff something is profiled.

fix

fix

Best parameter setting for de morgan.
-- This line, and those below, will be ignored--

M    tactics/paramodulation/saturation.ml

fix

if DISTRIBUTED all targets require a depend-stamp

:
This line, and those below, will be ignored--

M    tactics/paramodulation/utils.ml

profiler on steroids. added -profile-only to specify a regex to choose the profilings to print

removed mysql_escape that should be ok.... but adds some \ that make mysql
complain

added calls number

removed mention of the "library" target, no longer needed for the installation

fixed timestamp issue on tactics.mli

mock-up code for tactics contextual menu in the gui

Changed the type of compute-equality_weight that now takes also
in input the ordering

go

go

go

added raw query form

done

fix

Renamed SK.ma into bool.ma

Esempi di auto.

Snapshot.

removed \t

go

go

go

fixed wrong log name

ahh.....

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)