more lemmas and some generated logical constants for them

The name of the constructor for jmeq changed.

Bug fixed: when we try to add an object and it is not _directly_ well typed
(i.e. it is not well typed, and not because it depends on a non-well-typed
object in the library), we should not remember it, since the user can change
the definition and try again.

Use replace when switching tabs (see previous commit).

New function replace to be used in place of time_travel every time the user
switches to a new tab. In this way, every tab is independent and it only sees
the objects defined in that tab. This fixes the following bug: in tab A go
down; go down in tab B; go up in tab A (at this point also the objects declared
in B where removed); do something in B or go up in B (BOOM))

Dead code removed from the interface. It is used internally via references.

Changes to TeX-macro conversion.

Matitaweb: Bugfix for TeX-macro conversion.

Matitaweb: changes to utf8MacroTable.js

Matitaweb: changes to utf8MacroTable.js.

Matitaweb: TeX-like macro handling.

Changes to utf8MacroTable.js.

Added Utf8MacroTable for MatitaWeb.

More keyboard handling tests

- new definition of subst based on drop
- pr is now based on drop

more tests on keyboard handling.

more tests on keyboard events.

more tests on keyboard events.

more keyboard events tests.

more keyboard events tests.

more keyboard events tests.

more keyboard tests.

more keyboard events tests

more keyboard event tests

more tests with keyboard events.

minor bugfix

Testing keyboard events handling.

long file names caused indentation underflow (String.make) when times
were displayed

- some depend files
- bug fix in grafiteAstPp.ml
- some assertions in matitaEngine.ml

Added facility for resetting the library.

...

Added matitaweb administration panel.

Possible assert false case implemented

Removed filename input box from index.html (just browse the library now).

Fix to matitaweb library dialog box.

Fixes to library dialog box in matitaweb.

Opening scripts using the Library dialog (try 1).

More changes to matitaweb.css.

More changes to matitaweb.css.

Changes to matitaweb.js (dialog box).

Show library test 1.

More changes to matitaweb.css.

More changes to matitaweb.css.

Fix in matitaweb.css.

Fix in matitaweb:index.html.

Changes to matitaweb.css (dialog boxes).

Changes to matitaweb.css (dialog boxes).

More changes to matitaweb dialog boxes.

Second attempt at dialog boxes in index.html.

Bugfix in index.html.

First attempt at dialog boxes.

More bugfixes for matitaweb's viewlib.

Bugfix in matitaweb viewlib.

Matitaweb viewlib, part II.

Escaping exceptions are now captured.

Added viewlib to matitaweb.

missing ; to delimit syntax :(

More bugfixes in matitaFilesystem.ml

Bugfix in matitaFilesystem.ml

Changed user library dir to users/

Added generation of HTML representation of the library.

Some progress

ported reduction.ma

Ported par_reduction

ported substs and subterms

- xoa: more existential types
- ground: more arithmetics
- lift: more nasic inversion lemmas and some renaming

Unprotected List.fold_left2.

Remove the daemon :-)

New syntax of dummy with the type

Added a copy of lambdaN to extend the syntax of dummies with types

Added module MatitaFilesystem, to be used for the management of the library
in matitaweb.

Added location of the weblib repository to matita.conf.xml.in.

Added repository for the shared library to be used by matitaweb.

(Almost) working multi-user matitaweb.

Logout (partial work) (multi-user matita)

Multi-user Matita (and Matitaweb): added user authentication (currently only
tested on hard-coded accounts). Proof-objects are saved in a user-specific
directory.

some restructuring

more lemmas to prove and a correction in subst

more notation and one more lemma to prove :(

reductions rules and one lemma

more properties of relocation

Multi-user matita: changed the status object to include a ``user'' method
containing an optional string, used to identify associated user.

Fixes bugs in the  Matitaweb UI.

Fix for internet explorer (but still works badly).

Cosmetic changes.

Fixed a bug in the retract command of Matitaweb.

Logo for use in matitaweb.

Removed dependency of Matitaweb from GTK libraries.

- we removed the reduction-related item categorization
- some renaming

Removed hardcoded include paths from matitadaemon.

Some changes in the Makefile for matitaweb.

Fixes record projections (see matita 1.0 branch)

Matitaweb daemon ported from Ocaml Http to Ocamlnet's Nethttpd

This can happen: when you use nodelta.

Minor changes because of the new, weaker (but much faster) delift.

Bug fixed: trailing ' in names were not removed when computing the next free
name.

We reintroduce the distinction between binding and non-binding items.
Mon-binding items are now forbidden in environments

Major speed-up:

 1) bug fixed: the fo_unif applied to a metavariable in the subst made a
    recursive call using unify. Thus, in case of failure of the unify
    (after hints, reduction, etc.), fo_unif failed and hints, reduction,
    etc. was tried again. This resulted in an exponential blow-up in the
    worst case.
 2) bug fixed: in the case  ? args == ?pattern, the ?pattern was delifted
    w.r.t. args, but during the delift the special unification case with
    a pattern was considered again. This was costly since reduction was
    used on the first argument of the unification.
 3) semantics of fo_unif "fixed": it is now succesfull on every pair of
    terms whose rigid prefix is equal and whose arguments are unifiable.
    Before it used to fail for example on (x args == x args) where x is
    a Rel.
 4) BEHAVIOUR OF DELIFT CHANGED: it no longer matches terms in the local
    context up to full unification, but only up to fo_unif. Some tactics
    that used to be accepted could now fail and the user needs to change
    the terms by hand before applying the tactic. On the other hand, the
    speed up is really significant.

This update uses XML for client-server communication. For unknown reasons, this
doesn't seem to work well with Firefox (but works ok on Chrome).

We reverted to a single process http daemon because of an annoying bug in
Ocaml Http, causing the daemon to terminate randomly.

- we introduce extended existentials (generated)
- we exploit the tactic "*" to reduce the volume of decompositions