WARNING: this commit changes the DB representation; you need to alter the
         DB by hand after this commit

- h_position: varchar(255) -> varchar(62)
- h_sort:     varchar(255) -> varchar(6)
- several indexes have been redesigned from scratch.
  Motivation: MySql is not able to exploit two indexes (on columns c1 and c2)
  in a query of type "select ... from table where c1 = x and c2 = y".
  Only one of the two indexes is exploited; the other test is done on each line.
  My commit introduces a single index on c1 AND c2 in place of two indexes.

WARNING: it is sure that a few queries (e.g. match) are greatly optimized by
this commit. On the contrary I ignore if the performance of other queries drops.
Moreover, I have not optimized yet the indexes over the hits and count tables.

...

...

...

...

some fixes

...

Comment removed.

Paramodulation bug fixed.

Added datatypes/constructors.ma

New entries in nat: factorial.ma minimization.ma primes.ma primes1.ma
sigma_and_pi.ma

Added Z/plus.ma e Z/compare.ma.

The library grows...

Added q.ma.

ready for 0.1.1 release

integrated Eric's patch for HTTP/1.1 persistant connections

improved some comments

some bugs fixed

fixed compilation warnings

added homepage URL, now we have one

bumped standards version

do not install empty NEWS file

bumped timestemp, closed ITP

filled end user information

packaging cleanup: get rid of ancient debhelpers, use dh_install

ignore some autotools stuff

lablgtkmathview 0.7.2

Partial bug fix: every inner type is now added to the selection roots.
However, the inner types are not closed terms! They live in the context of
their terms. Right now there is a bug in locating subterms of a proof.
Thus I do not even try to fix inner types selection properly.

0. core_notation.ma splitted into coq.moo and core_notation.moo
1. 'include "coq.ma"' is now explicitly required to activate the notation of Coq
2. 'include "coq.ma"' added here and there in the tests
3. .ma headers updated

This test stresses automatic insertion.

The logo is now showed in the sequents_viewer window when there is no proof
in progress.

- re-factoring: dropped sequentViewer in favour of cicMathView which
  handles rendering of both sequents and objects
- added preliminary support for selection in cicBrowser
  (there are still issues with phisical equality and multiple xrefs ...)

Logo added to the about dialog.

1. ProofEngineHelpers.locate_in_term, ProofEngineHelpers.locate_in_conjecture
   generalized to return the list of matched terms
2. unfold generalized to unfold several occurrences at once

New tactic: unfold.

Bug fixed: unfold used to work iff the term to unfold was in head position in
the term.

arguments of ProofEngineHelpers.replace swapped.

bugfix: call add_selection_target each time selection changes so that
selection works more than once

Bug fixed: locate_term_in_conjecture used to raise TermNotFound as soon as
the term was not found in one of the hypotheses or in the conclusion.

added support for (textual) cut and paste of mathml/boxml markup

New tactic unfold.

added pretty printing of unicode symbols to TeX like macro

added attributes re-factoring item

added reverse mapping from unicode to TeX like macro (needed by rendering
to string of markup)

...

...

workaround for an assertion failure during rendering (missing sort of some ids)

removed orders_op from library (now in le_arith and lt_arith).

...

This commit re-commits version 1.61, removing the error (a "." in a regular
expression that did not match "\n").

REVERT OF MY PREVIOUS COMMIT THAT INTRODUCES A CRITICAL BUG (some lines
are automatically _removed_ from the script). I will commit again as soon
as I fix the bug.

Committing all the recent development of Andrea after the merge between his
commits and my recent commits (that added notation here and there).

More notation.

Management of automatic insertion of aliases and "goal" commands reimplemented
almost from scratch. The new commands inserted are now distinct entities in
the history. As a consequence going up in the script is now a step by step
operation and going up and going down are invertible operations, as they
should be.

Code simplification.

Bug fixed: added a _undoable_action critical section to the reset method of
MatitaScript.script to avoid a Gtk assertion failure.

dead code removed

fixed matitamake to handle development with names with spaces
the engine now has 2 different exception to report 2 diffrent problems:
- UnableToInclude
- IncluedFileNotCompiled

refactored gui handling code so that MatitaMathView is linked before MatitaGui
and all callback registrations happen in matitaGui.ml rather than matita.ml

...

matitaMisc.ml

safe mkdir implemented

proof of concept implementation of cut and paste from gtkMathView to text
(still via debug menu item "print selected terms")

renamed development related windows

added #proofConclusion

cosmetic changes

added get_proof_conclusione and list_tl_at

highlighted notation keywords

...

fixed cic_notation dependencies

better boxes (with more line breaking hints) for objects rendering

*** empty log message ***

bugfix: added xref on ast built via pattern matching from cic (3 -> 2)

added id_of_annterm: Cic.annterm -> Cic.id

bugfix: no more xref on bound names

added low level rendering attributes (indent, spacing, ...)

rendering from markup to string

improved debugging pretty printing of xref

"Coq's " prefix added to every interpretation.

Flickering bug fixed.

locate_in_term generalized to locate_in_conjecture

Comments added.

Bug solved: the #reparent method of Gtk should NOT be used:
see http://www.gtk.org/faq/#AEN636.
This solves the flickering problem that occurred when a new tab was selected.

Implementation of locate_in finished.

typo s/\\OF/\\of/

fixed typo in helpers for generating hv and hov boxes

draft version of locate_in_term

...

unreleased version of the bindings, with more gtkmathview method bounds and dependencies on gmetadom 0.2.3

...

**** Experimental: ****

After the disambiguation, if the term is no longer ambiguous, we forget the
environment. In this way we are forced to do more work later (since we have
less aliases), but we have more freedom (since we have less aliases) in the
future disambiguations.

typo fixed

"Coq's " prefix added to every interpretation.

Bug fixed: list_uniq o List.sort used in the lookup function to return only
one interpretation in case of duplicate interpretation definitions. This
happens when a module A defines an interpretation, it is included by B and
C and then a module D includes both B and C, thus defining the interpretation
twice.

bigger disambiguate chiuches win

...

More notation (up to where the open bugs allow me to put it without adding
too many aliases).

A little bit more of notation here and there.

some more changes and corrections

Notation for equality used everywhere.

Note: due to a bug in the notation machinery, the declaration of the notation
is a bit cumbersome (it uses a URI and an alias; it should use no alias and
just eq in place of the URI). To be fixed.