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)

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