added exists_meta

patched

updating the introduction

ported to latest polymorphic variant types

Added flag test_equality_only to are_convertible to better implement
the <=_{\beta\delta\iota\zeta} relation.

Added flag test_equality_only to are_convertible (to better implement
the <=_{\beta\delta\iota\zeta} relation).

added a missing <br> tag

implemented save_to

- uncommented save_to function (now implemented)
- added (tiny) description of the 'variable interpolation' feature

added Unix dependency (needed in order to run xmllint)

eta_fixing of the CurrentProof metasenv is wrong, since eta_fix does not have
the context parameter. Fixed by avoiding CurrentProof metasenv eta_fixing.

The parser accepts terms with metavariables as statements of theorems ==>
metavariable instantiation must be propagated also on the theorem statement.

- added test file

- added via_http parameter so that when the getter is used locally (i.e.
  as a library), http specific messages aren't generated
- use polymorphic variants for some configuration parameters
- better logging on /update (<br> tags are now generated)

- use polymorphic variants for some configuration parameters

bugfix: local context and canonical context previously don't have the
same length

bugfix: the function that abstract constant occurrences by putting metavariables
in place of identity explicit substitutions (local contexts) is generalized to
put ?1 : ?2 : Type in place of a ?1 : Type to take care of <Type in contravariant
position. Note: this is still partially bugged (see previous commit on the same
topic).

reorganized functions order

http_getter.conf.xml ==> /projects/helm/etc/http_getter.conf.xml

added html_of_html_tag

URL patching in ENTITY declarations extended to cover also absolute URLs.

XHTML character entities (used in the internal subset of .theory.xml files).

Added a new function in_cache to cicEnvironemt. It takes an uri
and returns true or false according to the fact that uri is or
is not in the cache

ht:DEFINITION/Definition differentiated into
 ht:DEFINITION/Definition and
 ht:DEFINITION/InteractiveDefinition

because of an explicit request of Iris Loeb.

s/per_user_settings/user_settings/ for consistency with gTopLevel
configuration file

- logging of long-running actions (like update) is now sent to the
  client incrementally
- moved some frontend related functions (like return_html*) from
  Http_getter_common to the frontend (main.ml)

removed no longer needed password from connection string

- added "Host:" line to http requests so that virtual hosting hosts are
  supported (and ancient HTTP are no longer supported)

- removed http_get/http_get_iter implementations, use the analogous
  functions from ocaml-http

<VARIABLE as="LocalFact"/> added

removed an out of date comment

added hyperlinks to help message

removed out of date configuration file

tacticChaser modified to avoid double "apply" and to avoid to apply uris ".var" in tactic "auto".

Meta files are in METAS subdir
source of meta files are called meta., not META.

Install to findlib-defined dest dir, not to stdlib dir

- provastruct.theory.xml removed (what was that exactly?)
- @name of SECTION renamed to @uri

updating and structuring

Algebra => CoRN

tex notation enabled

* the .o files to be used in the dll are now taken from the .libs subdirectoy
  (which presumably contains the PIC code)

CSC: hack to make applications of constants that have a Type sort which
occurs in contravariant position work. The idea is to generate in place
of a metavariable of type Type (that should be of type <Type) a
metavariable of type "a metavariable of type Type". The problem is that
in this way the metavariable can also be instantiated that is not a
sort.

* added embedding test (HTML)
* new things to do

* added TODO file

* added test with MathML really embedded within HTML
* set plugin border to 0 (? black line still visible)
* is set SHADOW_NONE the plugin window gets dirty!!! :-(

* implemented click so that the browser is notified with the new URL
  and loads it

cosmetic alignment change

- implemented real thread killing (in place of the previous fake implementation)

load_document(_,NULL) => unload

- power notation
- mult for BinInt

*** DANGEROUS ***
- multiple NUM instances now are different instances

...

introduction updated

The operational semantics of the core language is ready

Bug fixed for theorems whose statement are like

((A -> B) -> C) -> D

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.