Help for the first two tactics.

added splitting engine for .html generated by docbook -> xhtml conversion

no more dummy names for building the library in distributed tarballs

"sec_" prefix for section IDs

Added a few basic definitions of subgroups and left cosets (together with
their extreme notation!)

added instructions (some gaps still to be filled in, notably: ./configure
parameters and instructions on how to create the mysql database)

written install section up to build requirements

changed location of version.txt

added dir for released matita tarballs

- moved version.txt.in to the help dir
- added Makefile to generate xhtml and pdf from the docbook manual

reshaped manual

- use the best matitamake to build the library on dist
- renamed dist targets so that they are distinguishable and not callable in
  when developing matita

fill DISTRIBUTED value on dist

removed useless grepping -v

- factorization of the recursive rule
- added "library" target to build the stdlib when distributed
- implemented "distcheck" target

added configure time values SRCROOT and DISTRIBUTED

factorization of the recursive rule

added Matitamake interface

added last-modified info at the bottom of every page

- escaped "&" in URLs so that all pages are now XHTML 1.0 Strict valid
- expanded a bit the "nothing to see here" concept in the matita web pages

removed papers dir, now all papers are in the new "papers" repository

removed papers that have been moved to the new "papers" repository

absolute path and factorization for matita.basedir

- changed semantics of "init": now it is idempotent
- added support for "-v" flag printing "make" command line
- minor change: lazy discovering of whether we are ".opt" or not

use matita.verbosity instead of matita.quiet

- uniformed command line handling of matitamake with that of other matita tools
- changed "-q" flag semantics: now it reduce the "matita.verbosity" value by 1
  unit
- added "-v" flag: it increase the "matita.verbosity" value by 1
- "matita.quiet" is no longer in use

help path is no longer hard coded but relative to runtime base dir

fixed tactic ids to include a "tac_" prefix

- bugfix: pass -conffile to matitamake
- more quiet feedback during compilation of stdlib

Basic facts about group morphisms.

moved mathql/ under software/

first sketch of the documentation (to be used by yelp)

s/ocaml/components/ in the "tag" target

* groups splitted into groups and finite_groups
* a few lemmas added to groups

removed a Pcre capture that being _NON TAIL RECURSIVE_ used to cause stack_overflow... mah...

termine bacato.

fixed usage of matita.auto_disambiguation

Bug?

First proof on groups completed!

fixed download links and added underlined hyperlinks

on the fly generation of distribution configure.ac

added bg

fix

removed no longer needed libs link

Added abstract.

ported to the new svn architecture

- no longer need to dynamically discover if the components dir is libs/ or
  ocaml/: now it is components/(!)
- reverted default settings to the devel ones (debugging on, runtime dir=`pwd`,
  ...)

moved (dummy) dist stuff into software/matita/

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 :-(