first check-in of cic_notation

fixed whelp bar

fixed Whelp stuff

aded comment

cosmetic changes

bugfix: avoid duplicate entries while indexing (changed implementation
so that sets are internally used everywhere instead of lists, which are
now used only for implementing API)

- cathes more Mysql errors which could happen during post-indexing actions
- bugfix in hits table handling during post-indexing actions
- added copyright info

bugfix in elim, cardinality constraint should >= 1 not > 1

- no longer needs PXP
- added "interpolate" paramater to register iterators

added images

added examples

added comments, fixed history, added loadList to browser

some hacks to make the sequent window pretty nice

fixed instance

added comments

added saturation.opt to the ignore list

fixes (mainly) to demodulation and meta_convertibility

added support for hits table

added list and fill actions

sync script among databases

support hits table

sql for filling hits table

added hits table

better table creator

added "all" table meaning "act on all tables"

fixed

fix bad space

now the extractor manager renames the tables (old tables are renamed to _BACKUP)

some more statements

added index on refRel and the rename table statements

- ported to new ocaml-http API
- uses Arg for cmdline parsing

exported new_metasenv_for_apply, needed by the paramodulation stuff...

fixed demodulation bug

moved string_of_equality into utils

first commit of paramodulation-based theorem proving for helm...

fixed memory leak (workaround)

fixed Makefile

fixed a TODO comment (MUTCASE _is_ implemented)

handling of variables with body

handle XmlPushParser.Parse_error exception

added Parse_error exception and pretty printing of Expat errors

more detailed info about peon's problems

ignores test and test.opt

- changes defaults of getxml (format gzipped, don't patch dtd)
- big bug fix which avoid spurious \n at end of gzipped file

moved up xml, now needed by CicParser

make use of gzipped type and body

moved xmlPushParser in ocaml/xml/ since it does not depend on cic

made optional dependency on thread library and compile time flag

added dep on expat

ocaml/ todo list

moved here xmlPushParser.ml and corresponding test

added 'tags' target (which index both matita/ and ocaml/ above)

The README file was patched

Toolbox: preliminary version

added syntax for rewrite (TODO no rewrite-in-Hyp syntax)
bold sequent line
more space between the sequent line and the formulae

factorization of rewrite.
now the tactic also does a beta reduction step
(behaving as expected)

- ported to new CicParser interface which requires an uri argument to be
  passed to parsing functions
- removed orrible hack for sort parsing

added "tags" target to generate vim tags with otags

added test and test.opt targets

- implemented CicPushParser which parser CIC objects using Expat
  (currently, old PXP parser have been renamed to CicPxpParser, new one
  has been named CicPushParser and CicParser can includes one of the
  two. It includes CicPushParser per default)
- added mandatory uri parameter to main parsing functions, it is needed
  for creation of universes when Type sorts are encountered

- added .cvsignore
- removed test.ml (which has been promoted to extractor.ml)

test_instance.ma

Some modifications due to instance.

added .depend

added extractor_manager

added new extractor based on MetadataDb.index_obj

sync with SqlStatements

added DROP statements to sqlStatements

more friendly sqlStatements api

added examples

added table_creator (comman line frontend to SqlStatements)

added sqlStatements module (contains all CREATE TABLE/INDEX)

added instance

fix for instance

First version of instance.

attached auto

attached auto

added the count table

added Match (partially) and sync with the count table

added ast for Match

removed no_inconcl_aux, no_concl_hyp, no_hyp and added count

added more assertions on universes when loaded from dump (and fixed some bugs concerning re-hash-consing)

added the orrible hack to the parser that is needed to call CicUniv.fresh() properly

hint -> experimental_hint

main constants set is closed with constants types

UniverseInconsistency is now wrapper by CicRefine.type_of_aux' to RefineFailure

no more moogle... now whelp (config file name and daemon name)

added dump/restore environment to the debug menu
fixed bug: when proof is completed the browser@home is blank

added orrible hack to make the current uri visible in the parser so that named universes are generated

catched UniverseInconsistency
(only an hack, it should be wrapped by the refiner)

added parsing time benchmark
universes generation counter is now properly reset
added orrible hack to make the parser generate proper universes containig
  the uri

fixed a typo

added parser benchamrk

fix (ask Enrico :-)

uses CicUniv new assertions

added assertions about graph in the environment having Some uris

added rating parameter to at_least (used by elim)

attached macros: hint(partial), check
now matitaScript has a mathviewer to show terms...

moved "hint" from Command to Macro

deactivated coercions