Sorts are no longer all convertible. To be completed once that universes are
implemented.

Sorts are no longer all convertible. To be completed once that universes
are implemented.

This fails.

added final version of the paper (for the records)

talk committed

updating

New tactic Auto.

First implementation of the Auto tactic.
- tacticChaser: added a function to locate all the theorem tha can be applied
- variousTactics: the Auto tactic

Type of exception changed: from exn to string.

- interpreter: the queries are printed before execution
- generator  : a bug in the generation of isfalse clauses was fixed

interpretation_choices not declared

escape/unescape no longer works with '+';
replaced with encodeURIComponent and decodeURIComponent

Parameter forgot.

Partially ported to new disambiguating parser.
Some bugs left (e.g. in aliases)

Debug code removed.

Dead code removed.

- non empty metasenv after the parsing phase are now accepted
- still many bugs open (due to the new aliases for symbols)

Bug fixed: instead of generating "not ()", I generate "true" (for PostGresql)
and "1" for Mysql.

Meta no longer raise a failure. Instead they return an empty set of
constraints. This is just a temporary patch. To be understood.

- reindented
- "count (" is not valid SQL (at least for MySql).
  Replaced with "count("
- binary removed. Tables are now binary by default.
  The advantage is that in this way indexes do work.

Disambiguation can now return more than one choice.

Quick & dirty patch to overcome a bug of ocamlfind.

Added option -timeout. Default is 5s.

\Assign and \subst to match the parser.

MutCase branches must be parsed and printed using \Rightarrow.

Branch of MutCase must be parsed and printed using \Rightarrow.

Debugging message removed.

apply_subst did not apply the substitution to the explicit named substitution
(local context) of a variable.

Refine now raises only RefineFailure, AssertFailure or Uncertain.

Wrong error message patched.

List.nth not guarded by try ... with. Fixed.

Debugging code removed.
Query logging is already implemented. It can be activated from the
.conf.xml file.

HelmLogger logging function connected to MathQL Interpreter logger function.

Syntax of explicit named substitions syncronized with the parser.

Yet another error in the id regexp: numbers are allowed in identifiers, as well
as 's.

Bug in guarded_by_destructors (case Rel to a definition in the context) fixed.

Big bug fixed: batchParser applied the varsprefix prefix also to
constants and inductive types!!!

It is now possible to specify independently the prefix for variables and
the prefix for all the other objects.

Improved output when [ MANY ] occurs.

...

...

- Improved error messaging.
- Invalid_argument was raised by List.fold_left2 ;-(
  I want checked excecptions!

- ported to latest CicAst.Ident format (Some [] <> None)
- unspecified local contexes are now inferred

differentieted empty substitution list from no substitution given

- regtest now handles more than one interpretation: the tests committed
  here have been ported to latest regtest format
- more informative failure report

added cast concrete syntax

The regression tests now check also the generated disambiguation environments.

Regtest fixed. It can now work also with multiple answers.

The disambiguation now returns a list of interpretations.

Note: the regtest is broken by this commit.

The disambiguation now returns a list of interpretations.

now database interfaces are more abstract

- MySQL mode added to the interpreter
- hxp restored

Error message fixed.

...

triciclo.conf.xml ==> gTopLevel.conf.xml

Added () to MQInit.init.

New implementation of eat_prods. Some residual problems disappear.

New implementation of eat_prods.
In theory we expected it to be less efficient.
In pratice it is MUCH more efficient.

The old implementation is still there, but commented out.
We have to investigate the mistery a bit more.

- better handling of temp files wrt to failures. When a temp file has
  been created and an exception is raised, the exception will be
  catched, the tempfile deleted and the exception raised again

added support for commands and scripts

added vim modeline for encoding=utf8

added command and script ASTs with _debugging_only_ pretty printers

Bug fixed: names of just one character were not inserted into the objectName.

One MQInterpreter commit broke regtest.ml. Fixed.

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