sandeich lemma makeup

Restructuring.

Main inequalities for e.

Added summation formula for the power of a binomial.

the is_structure is a bad idea if you don't have canonical structures.

Binomial coefficients and costant e.

A few more theorems.

dump spurious errors max

excede->excess

excedence -> excess

weight -> value

dump result table in \TeX format

...

Repeated errors are not duplicated.

Even if the error is not localized, it was not a good idea to make the unification error
escape.

refactoring of some lemmas, shorter proofs

Some terms are not localized from the very beginning :-(

Added debugging option to ask for all disambiguation errors (even spurious ones) in all passes.

One more error localized. But the code is really ugly here :-(

added do_heavy_checks documentation

do_heavy_checks not always true, take ths option from the registry instead

added do_heavy_checks default

if parameter type is given, this assert is false

Only errors from passes 4 and 6 are kept.

Reindented.

sandwitch theorem done

removed all the axioms!!!

sligtly more general results, still to reorganize

ok

1 lemma left!!!!

Some progress.

Forward compatibility with new lablgtk2.

carabinieri almost done

carabinieri almost done

cleanup of the eq_trans burdain

3.11 !!!

added a way to generate all the utf8 symbols

Dead code removed.

Bug fixed: an unification exception used to escape during eat_prods.

more stuff

...

Output is now in UTF8 character counts.

Options declared but not parsed.

Ported to camlp5 < 5.00

Back-ported to camlp5 < 5.00.

....

...

remove debug fake data

(hackish) scripts for testing spurious disambiguation error criteria

add "-order" cmdline option to just print a possible build order of the given *.ma files and then quit

change naming scheme for rottened script, so that they do not mess up matitadep/make assumptions

...

major reorganization (read cleanup)

bir georganization, most of the structures done

avoid rottening of constructor names in pattern matchings

ignore sqlite db and rottener* executables

- use "O" as the rottening token
- add generation of a trailer with error location information

make target for cleaning rottened files

reorganization of many files according to the new basic picture.
todo: premetric lattice and the various coercions

first draft of a script to mechanically introduce (disambiguation) errors into Matita scripts

ignore *.o

add dump of position information in the lexed file

Axiom moved from ex_deriv to deriv where it belongs to.

Notation improved.

Some code clean-up.

Disambiguation error compaction is now performed in the same way by matita and
matitac. The difference is that matitac shows every error in every pass,
marking spurious errors as spurious.

for csc

pretty

Patch to automatically generate filename.error.md5.ma scripts every time a
disambiguation error is faced by the user.

Almost there.

This version of disambiguate.ml implements yet another (better?) criterio for
spurious error detection. An error is spurious iff:

a) it is obtained interpreting a symbol s using an interpretation \phi
b) there exists another interpretation \phi' such that
   1) dom(\phi') = dom(\phi)
   2) \phi' is valid

It should be true that no nested error locations should occur.
In principle this also suggests the possibility of changing the user interface
to show all alternative errors at the same time.

Bug fixed: an unification exception used to escape when coercions were disabled.

since the previous commit fixed some bugs when the context has a deleted hp,
the script is better

restored the right context used to generate names. see the comment

This alternative version of disambiguate.crit2 implements the following
criterion for spurious error detection:

an error is spurious iff:
  a) it is obtained interpreting the symbol s with the interpretation \phi
  b) there exists another interpretation \phi' such that
     1) dom(\phi) = dom(\phi')
     2) \phi' is valid
     3) \phi(x)=\phi'(x) for each x != s

More (but not too many) errors are spurious according to this criterion.

fast and sound registry lists
faster matitamake setup

* NOT RELEASED YET

* bump deps on lablgtk2 to match lates upstream
* debian/control
  - fix VCS field names (now supported natively by dpkg)
  - add Homepage field

lemma finisced

Bug fixed in printing of passes in error messages.

lemma 3.57 half done!!!!

notation in autogui

Big progress

snapshot

Very incomplete example of simple calculus exercises in Matita.

...

opps, a changelog was already there

Bug fixed: local type declarations are not allowed in ocaml.

...

Towards chebyshev.

The axiom can be proved. Just follow the hint.

fixed bugs found by csc

moved to pkg-ocaml-maint

Some notes for Enrico.

...

hidded publish-devel button, too dangerous for the casual user

hidded all hbugs related stuff

from the tarball removed all contribs, they used to weight more than 1MB
and were not compiled nor installed

...

...