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

changed binding strength of some parsing entries:
( a > b means a binds more tightly than b)
- now: infix operators > binders > application
- previous: application > infix operators > binders

removed spurious debugging prints

html-escapes user given expression when filling hidden field "expression"
in this way xml/html forbidden characters like "<" are converted to "&lt;"
and doesn't crash uwobo

bugfix: opt target should build html pages too

added clickable fingers

changed logo: whelp!

the description file was patched

initial version of the "lambda-delta" calculus including:

- Confluence of reduction
- Generation lemma
- Thinning lemma
- Substitution lemma
- Type Correctness
- Type Uniqueness
- Subject Reduction

debian version 0.0.5-6

rebuilt against ocaml 3.08.3

debian: rebuilt against ocaml 3.08.3

remove x_gdome_caml.c generated source on "clean"

debian: rebuilt against ocaml 3.08.2

Bug fixed in assumption_tac: a missing (lift n) when a declaration
x : A := t is found in the context.

- bugfix: do not fail when query_kind is missing (e.g. on /getpage)
- bugfix: security, no longer subject to directory traversal (!)

user smaller font in result page

- new pretty printing of interpretations
- bugfix: interpretations are now remembered between pages
- more coherent look and feel