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

make and clean also in html/

removed old HTML files (tagged with "old_htmls")

moogle.html is now generated, it do not needs to be in CVS

generate HTML templates using XSLT starting from a bunch of .src files

look and feel improvements

- re-enginered main moogle template, it is now aware of queries kind, summary,
  and results. This enable fixing of minor like feedback on the query kind in
  case of errors
- minor bug fixes: 1/0 nuisance in case of errors
- commented out advanced query selection (which do nothing)

- handle metavariables: if at least one of them is present, then the
  cardinality constraint is not enforce
- commented out debugging prints

bugfix when user query contains metas: their context should not be analyzed
as it were in main position

Bugfix in restore_from_channel, before this fix hashtable (which has uris as
keys and pairs <objects,universe> as values) was dumped but restored as if it
have uris as keys and objects as values. That caused immediate segfaults
while trying to iterated on the restored table.

added support for open terms in check

support for terms with metas in check

added choose_uri method to console, used by the interpreter to implement the
hint command

Added heuristic in the Appl case, we beta-expand only if the argument list
does't contain metas.

Fixed remove operation and get_obj (that now correctly searches in the
unchecked_list).

moved a debug print so that it is executed for each phrase

adapted to optional comment lexer interface

renaming "remove_term" -> "remove_obj"

- fix in intro parsing
- avoid generating seq tactical for a 1-length sequences

factorized tacticals separator and terminator