Optimization: since an invariant says that the inferred type of a term is
always a type, then we do not have to call the sort_of_prod to check the
the type of a lambda-abstraction is a well-typed prod. We just have to check
that the source of the lambda is a sort (or a meta).

...

eqT removed.

Variable redefined. Fixed.

added mathitaGui.mli

snapshot

added functions and uris for binary {positive,integer}

added binary {positive,integer} notation

New v8.0 URIs.

More uris ported to V8.0.

More V8.0 uris.

More v8.0 URIs.

Porting URIs to V8.0.

Partial porting to V8 URIs.
Almost nothing has been tested yet.

Porting to MySql.

MySQL is case sensitive.

Quick patch to make everything work with MySql.
Note: to compile you need to make a symbolic link from mQIDataBase.ml
to mQIPostgres.ml or mQIMySql.ml

- added support for boolean parameters
- added support for optional parameters

...

- Targets reorganized
- new targets

Added parameter format=text|xml to getalluris.

A lazy value was put in place of a function ==> the memoized value was no
longer updated. Fixed.

"add_server?position=0" no longer worked (raised an assertion failure)

No longer in use.

Script to create and drop tables and indexes committed.
New targets added to the Makefile.

added a space between term and "using" keyword

commented out a debugging message

bugfix in "elim ... using" tactical ("using" is a keyword)

added a lot of notation: arithmetic operators, relational operators, ...

Rinv typo fix

-memory leaks fixed
- INSERT INTO objectName .... was not quoted correctly

The metadata extractor now generates also
"INSERT INTO objectName ..."

New framework for metadata generation.

NOTE: from this release on the metadata are inserted into a MySQL DB.

(Very)* Old stuff removed.

Bug fix: the generated XML for DCs was not well-formed.

kind=dc implemented.

support optional keys in configuration file

removed password entry, now uses "helm" user (read-only access is
enough for rdfly)

* update for 0.0.5

* cleanup

* fix so that ocamlmklib works

* removed debian dir from EXTRA_DIST var

* using non-diffing mathml factory
* removed methods no longer implemented in gtkmathview from interface

* updated the updating method so that the root element is not changed
  (removes the listeners in the new editor)

* added wrapper element around processed document

* fixed profiling flags

...

first check in of mathita gui

bugfix: "in" is an IDENT, not a keyword

Quick patch to use rdfly (URL hard-coded everywhere).

hard-coded timing of generated queries disabled: use T interpreter flag instead.

Ported to
 - Helm_registry
 - Mysql

- mathql interpreter flags reorganized
- logging function in NQIConn.init is now optional: default is ignore

A brand new daemon: rdfly.

source logging patched

new mathql interpreterr flag V

source logging is now native in the interpreter

source logging enabled by default

Adding tacticAst2Box (pretty printer for tactical, preliminary version).

Minor modification in test_parser (to use the new pretty printer for
tacticals).

...

mathql interpreter flags can be now red from helm registry

...

uwobo ==> uwobo.opt

...

Stuff moved around.

ENVSCRIPT and mathql_db_map.txt no longer in use.

Removed stuff no longer in use.

helm_registry is already in due to transitive dependencies

The order IS significative. Changing the order (in one of the last commits)
broke the ls method.

typo fixed. Used to break the ls method.

- better error message on "unknown identifier"
- use newer (Andrea and Luca)'s box-based-pretty-printer

fixed cosmetic typos during pretty printing

- bugfix in term grammar: lowered precedence level of "let ... in" so
  that "let x = 1 in x + 2" works as expected
- decent grammar for tactics and tacticals: now with precedence levels
  (no more stackoverflows, hopefully)

catch parse error exception and show them to the user during main loop

patched

batchParser and regtest patched to avoid a non encapsulated connection to the mathql interpreter

Bug fixed: Helm_registry was used not enough lazily (i.e. before loading
the configuration).

added copyright info

removed useless Mpresentation module

moved away tactics and tacticals

added tactics and tacticals (heavily bugged)

added hook for .cma link time options

added tactic and tactical (still heavily bugged!!!)

68080 (that overflows ; -) ==> 38080

fixed typo

New key postgresql_connection_string.

removed (now useless) connection string line

New key mathql_interpreter.postgresql_connection_string.

The PostgreSQL connection string has been moved to the Helm_registry
(key mathql_interpreter.postgresql_connection_string).

Other stuff no longer used removed.

Several no longer used variables removed.

Porting of applyStylesheets.ml to Helm_registry.

Reindentation.

mathql_db_map.txt now retrieved by Helm_registry.

mathql_db_map.txt is now retrieved by Helm_registry.

-linkall removed

- ported to Helm_registry
- ported to the new disambiguating parser of Zack & Andrea

searchEngine ported to Helm_registry.

fixed typo