A few paramodulation/demodulation tests moved from library to tests.

Big bug fixed: attributes of constants were forgot during parsing!

Cambiamenti nella parte sulla disambiguazione.

- added some cicbrowser screenshot (to be better placed in the text body)
- added list of tables (and thus ignored .lot files)
- moved graphic files in the pics/ subdir

use italic by default

indentation

A failing unification of a coercion vs a term is now tried again after
a delta-beta weak head reduction of the coercion. This is necessary to handle
the case (f (g ?)) vs (fg t) where f and g are coercions and fg is the
composite coercion.

As a result the notation in algebra is now nicer and more notation can be
parsed.

no longer requires old diagrams

removed libraries old dot

removed an old figure

removed old version of the matita paper

spell checking

ignore .log

some more fixes

snapshot

reshaped the "authoring interface" part

added .dot which generated libraries-cluster.{ps,png}

added klocs sums and heading "0." where missing

- added components diagram with KLOCs
- fixed some dangling references

added generation of KLOCs in dot diagrams

New formulation of finite_enumerable_SemiGroups to allow the \iota notation
to be invertible. However, this does not work (yet) in practice due to
unification between a coercion and a composite coercion. E.g.
 (composite x) vs (f (g ?1))

First part of a slightly more interesting proof on finite (and enumerable)
groups.

6hands-introduction to the last two sections

added gluing among patterns and semantic selections

added entry "on the roles of mathml/latex"

bugfix: demodulate_tac is in module Saturation

Code restructuring.

Added some examples for auto/paramodulation/demodulation.

added kluwer latex style manual

centered screenshots

added some screenshots

added undamaged version of the icon

removed damaged icon

right and left cancellation in groups

section re-ordering

Cenni alla disambiguazione lazy.

ignores .toc

- s/decompilation/cleaning/
- highlighted some (un)interesting points in the (de)compilation part

reviewer compilation/decompilation part

completed disambiguation part

labels here and there

uniformed (G|g)etter with \GETTER

- towards completion of the disambiguation section
- some \MATITA and \COQ here and there

- use "sec:libmanagement" as label for compilation/decompilation (it was not
  uniformly used before)
- typos in the disambiguation section

added proof of SN for T+ind

draft of compilation/decompilatio

Yet another strategy for let...ins: a let-in is _NEVER_ simplified.
The user has to use unfold to zeta-expand it.
(Thus, a let-in is more opaque than a constant in the environment.)

restructuring

Improved rendering of conjectures

more structured and indented version of nat.ma

bugfix: when looking for a goal from the continuationals stack handle the case that no one is there (i.e. the proof is completed) avoiding run-away exceptions

added a smaller version of the icon

Added header to all files.

Added header

looks fine to me

- moved section in place according to new organization
- commented the (missing) screenshot to enable compilation

new version

Matita header

font -1

Updated version

New reduction strategy (that behaves much better during simplification).
Unfortunately, the new reduction is a bit slower on one test (paramodulation).
To be investigated.

1. Back to nicer (and more comprehensible) notation (that cannot be used
   when more than one structure is in use at once).
2. The first definitions and theorems over groups.

"Hiding" notation for implicit coercion. Cool.

Some work...

A few experiments (with horrible results) using notation...

Aggiornato alla nuova gerarchia di moduli.

debug prints commented

some debug prints/stats

library ==> component

paramodulation is no longer a self-alone module

baseuri of coq.ma fixed

libraries.ps no longer in synch.

New dependencies!

Universes speedup:
1) the merging is done thinking that the working graph is probably bigger than
   a cleaned ugraph
2) a cache of already merged ugraph is added.

fast hack to fix decompilation with -nodb with the new getter.prefixes format

changed universes merging order: euristic which improve performances

Bug fixed (in Cast).

An embryonic kernel of the algebraic library.
Useful only to profile the universes :-)

subst_vars optimized for the explicit_named_subst=[] case (the most common
one)

Dead code removed and reindentation.

(Partial commit)
Improved version of cicReduction. Configurations can now be preserved as much
as possible (without need to go back to terms by means of unwind).
This allows the implementation of new strategies and removes a few sources of
inefficiences.

The commit is partial since not every strategy has been ported yet.

...

Bug fixed: the wrong context was used.

Dead code removed.

bugfix for missing parens: when the precedence does not change, parens are now added not only when there is a mismatch Left vs Right or vice versa but also when there is a mismatch Left vs Inner, Right vs Inner and vice versa.

Added recursive path ordering and demodulation tactic.

More informative error message.

fixed coercions undoooing

fixed

fix

fixed compilation order

fixes for paramodulation relocation
saturate(.opt) is now always compiled

fixed paramodulation trnsition

Removed calls to paramodulation.saturation.init

Moved paramodulation inside tactics.
Added a new (reduction) tactic demodulate.

ignore used to avoid Y warning

Dependency coq.moo.opt added to target tests.opt

Dead code removed.

Dead code removed.