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

some work till the need of redoing all groups based on excedence

since there is no more tab, the modification of the current file is in the window title

- destruct tactic: automatic simplification in case of failure removed
- library scripts: changed accordingly
- LOGIC: injection lemmas for the coercions added and applied where neaded

Note: destruct does not whd the equality argument as the old subst did

removed ugly printing

ordered_sets are built with excedence

added ordered sets

renamed ordered sets into excedence.ma

relocated

removed dust

HIDDEN (since glade do not read out file properly anymore) tactic bar and
outline notebook tab

new file with some relations stated in Type

ordered set is over, much new stuff coming from a coreflexivee/cotransitive
execedence relation.

refactoring

old subst tactics removed. New destruct tactic used instead

a) Detection of existential types now implemented
b) New heuristic for pretty printing of type definition arguments.

More correct (but still bugged) implementation of type definition.

Dead code removed.
More ocaml keywords.

snapshot

...

- subst tactic keyword removed from highlight syntax tables
- svn:ignore property fixed for Base-2 devel

Trivial bug fixed in type inference of LetIn source types.

xxx