* convert the package to a non-native Debian package

* debian/rules: instead of passing explicit -I flags to ocamldoc, do them
  via ocamlfind and OCAML_OCAMLDOC_OCAMLFIND_FLAGS

overwrite old symlink upon dist

ignore tons of generated stuff

* convert package to a non-native one (closes: #457353)

* promote Vcs-* fields to real debian/control fields
* update standards-version, no changes needed

beginning proof of chebyshev's bound on prim.

accepts the poly shape for gviz maps

upper bound for logarithmic summation

A few more lemmas.

Much more verbose statistics.

Bug fixed: \n prevented recognition.

Some inequalities.

Progress.

add support for adding identifiers instead of only changing them (enabled per default)

Partial progress.

more chosmetic

Main result for e.

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