Abstract and conclusions.

Snapshot

Snapshot

line breaking

spell checking

Pigeonhole proof restructured.

Some more work on the proof of the pigeonhole principle.
Really tougher than expected.

Bug fixed in generalize: a status was generated with an old metasenv.

added fix for marangon

use math mode when referencing terms from a \sequent environment

community review, solved a couple of TODO

/me finished reviewing ...

/me reviewed section 4

fixed

fixed ocamldep command line

/me reviewed automation subsection

fix

fixed some depends

Bug fixed: metasenv used in place of metasenv' during rewriting in an
hypothesis.

/me reviewed section 3, here I go ...

minor fixes to ENGLISH
added CoqArt book

Added a new section on automation

some makefile work

/me reviewed up to section 2 (included)

A new TODO.

Some more progress in the proof of the (ad-hoc ?) pigeonhole principle.

added a couple of todo items

fixed cmi:cm(x)a problem in makefiles

snapshot ...

Un TODO rimosso.

System section "completed".

Rewriting steps using the rewriting principles in the library of Matita are
now supported.

- use kluwer bibtex style for numbered references
- do not ignore .bbl any longer

- minor corrections in the disambiguation section
- better screenshot for the authoring interface

structured a proof

correct name entry {Sacerdoti Coen} in bibtex

CSC/Occam chain-saw/razor on tinycals and library generation/invalidation.
minor changes on patters terminology.

uniformed terminology used in the indexing part to that used in the rest of the paper

- recreated cicbrowser related screenshots
- minor corrections (mainly TeX macros) in the indexing part
- described cicBrowser in the library part, moved there screenshots, ...

Typos

Draft of section Indexing and searching.

uniformed disambiguation part

Added whelp to the repository.

few bits for coq comparison of patterns

chosmetic

tidied .tex

tidied .tex

1. The last commit that fixed unification of compound coercions with
   applied atomic coercions used to introduce too many compound coercions
   at the end. In this commit we fix the problem in a brutal way by
   mergin coercions every time CicMetaSubst.apply_subst is called.
   To be refined later on.
2. Several bug fixed in coercions handling. In particular, a coercion whose
   source or target was a name was given an invalid URI and was not unified
   and applied correctly.
3. New version of the algebraic library. In this version we differentiate
   between pre-structures and structures. This allows a few theorems/lemmas
   to be stated in a more natural way.

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