(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

...

...

nocomposites

compose tactic restore and added nocomposites keyword

more cleanup

...

added recommends graphvi

...

xxx

added homepage field in control

fix

fix -noinnertypes set to true!

removed dummy MATITA_CFLAGS assignement

added default for matita.noiinertypes

menu fised

propagation of noinnertypes to matitac

added -noinnertypes

...

cleanup

cleanup

declared eq_sym as a coercion and added 2 lemmas for rewriting #

...

autobatch => [auto]

...

...

removed prerr_endline

removed ugly prerr_endline

added --version to allow help2man

added manpages

...

matita-icon

...

...

...

wrong dependency removed

changelog to -rc-1

...

rc-1

added ~delta parameter to saturate_term and used it when saturating a coercion.
it is always true that the user wants the type of its coercion no to be
unfolded, since its arity was computed without unfolding.

Bug fixed: yet another case where tys of mutual recursive functions were not
lifted correctly when pushed in the context.

xxx

now destruct takes an optional list of term rather than a sigle optional term

fixed notation

ogroups almost finished

snapshot

snapshot

End of groups :-)

snapshot

- ProofEngineHelpers: namer_of moved to GrafiteEngine
- DestructTactic: unexported destruct_tac now uses lazy terms

previously hidden simplifications (in old destruct) added