moved toplevel makefile to sfotware/

- renamed ocaml/ to components/
- moved components/ and matita/ below software/

removed no longer used METAs

do not delete Makefile and Makefile.common on distclean since they are no
longer generated at configure time

made "dtd_dir" optional, is needed only by the web server, not by matita

added build time configuration of the whole components/ dir

bugfix: mkdir now works also for realtive directories

release snapshot
- split of multiple matita conffiles (users vs developers)
- removed no longer needed keys in conffiles
- commented conffiles entries
- made matitaInit.ml more like other matita tools (still a lot to do ...)
- save .xml debugging files only if debug is enabled
- ...

release snapshot

snapshot

Modified lambda and explicit substitutions.

cosmetic fix

added DBHOST & co ...

default of auto_disambiguation set to true

svn:ignore updated

- moved images in images/
- now all pages are valid xhtml 1.0 strict

use server-side include

added images and links for validation

fix

fix

fix

a further step toward releasable Makefile

Some more work...

reorganization continues ...

(dis)organized web stuff

daemons tamed

dir reorganization

moved some old stuff to the history

removed "tilde_expand" hack: for the moment it is not needed (we can use $HOME)
if it will be needed in the future it should be implemented (properly) in the
registry itself

removed no longer used coq_notation_script from API

added fallback to environment variables when a key is not found neither in
the XML nor in the mangled name
setting something like:
  <key name="foo">$(HOME)</key>
now works as expected

release work snapshot ...

added meta targets all, opt, ...

snapshot

no longer ignore Makefile.defs

no more multiple configure/Makefile, just one for both ocaml/ and matita/

working on the release ... la la la

more style fixes

No longer valid comment removed.

- "ocaml/" -> "libs/" in the distribution
- fresh copy of configure.ac

release snapshot ...

ported to the IEEE latex8 style

added (placeholder) distribution stuff for matita

removed obsolete library installation dir setting

moved dot stuff to STATS/

moved mathql metas to mathql/

moved mathql side by side with ocaml/

line breaking

near to the final version ...

review on csc's latest additions

added links to svn tarballs

Closer to the proof of the pigeonhole principle... that is already in the
library as a theorem over permutations :-(

Bug fixed in generalization: the goals opened by lazy parsing of the
generalization argument were not reported correctly. This fix is not
100% correct, but it will do for now. The best solution would be to
add a new tactic to modify the metasenv and to make the status type
private.

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