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

single INSERT on multiple tuples
cosmetic changes
vars are now indexed

added hbugs and mathql

renamed hbugs hint costructors to match latest API

bugfix: patched .ml.in instaned of .ml :-(

checked in new version of matita from svn

removed all matita files

removed all old matita files (kept in attic)

ported to svn-cvs merge

merged changes from the svn fork by me and Enrico

make also in utilities on whatever target

cvsignore

removed ancient cic_textual_parser (last live version tagged "dead_dir_walking")

added re-hash-consing of URIs embedded in universes

getter with in memory tree of URIs

better checks on elim input, two conditions are now required for an
input to elim to be valid:
1) before the disambiguation an indentifier has been given by the user
2) after the disambiguation a MutInd Cic term has been created

clean also hypno_tbl

added test.opt target

- ported to current metadata API
- changes so that it does not index a single URI given on cmdline, but
  rather all the URIs contained in a file

added sample entry for environment_dump configuration variable

added CicEnvironment preloading

added licence header

added license statement

added license header

made context and metasenv parameters of trivial disambiguator optional

added Trivial module with a disambiguate_term implementation which took
a string as input and return a Cic.term (if the input is not ambiguous)

removed debugging print

uses new at_least with criteria on constants number difference

added filtering criteria on differences between number of constants in
hypothesis and conclusion, should handle better queries on terms with
metavariables

- added no_hyp table
- changed constants number integer type to small int
- added comments describing tables

split precedence level of binders: \lambda has higher precedence than others
this is the resulting precedences scheme:
  lambda > apply > infix operators > binders

removed ancient indirections for gTopLevel

no longer build neither mathql nor hbugs per default

bumped copyright years

utilities for creating environment dumps

(hopefully) final decision on precedence levels:
  binder > apply > infix operators

bugfixes:
- reference position using MetadataTypes.*_pos so that changing the
  position prefix fixes all the references
- don't generated dummy predicates which always suceed like ("mainConcl" OR
  "inConcl") for at_most checking