New change in patterns: the pattern "in H" is now interpreted as
"in H \vdash ?". It used to be interpreted as "in H \vdash %".

The refined form of a reference to a let-in bound variable in the context
used to be the zeta-expanded form. It is now the reference.

use uniform naming for referencing cicNotation* modules

...

removed tedious debugging message

avoid generating multiple times the same xref/href

fix generation of applications of applications.

added @raise in comment (and source)

simplify and let-in

...

Assert false (for imbricated theorems) changed to a nice error message.

New strategy for let-in unfolding (aka zeta reduction): a reference to a
let-bound variable is expanded if and only if the simplified form of its definiendum (applied to the actual arguments) is different from the
non-simplified form.

Critical bug fixed: the get_cooked_obj was called on an object that was not
in cache. The bug did not manifest when the environment was trusted.

Typing errors fixed.

The logo was searched in the wrong directory.

Bug fixed: Invalid_argument was raised by List.combine in place of a typing
error. A similar thing occurred during pretty-printing.

LAMBDA-TYPES moved under contrib, fixed (to use the library of Coq even if
the library of matita is already compiled) and added to the daily benchmark.

bug fix for IDA: uses remote names (i.e. http://..) when patching xml bases so that external links like images gets valid URIs instead of invalid local ones like /tmp/...

LAMBDA-TYPES moved under contribs

The popup that asks to generate .moo for a .ma shows only the basename and not the full path of the file.

Bug fixed: matitac used to stop too early when an ambigous identifier was met
and auto_disambiguation was true.

create_owner_environment missing from matitatop initialization

...

Unsharing removed since it is now used in Cic2acic.

Unsharing finally introduced (but just for object processing, not yet for terms
and sequents).

Bug fixed: sorts and implicits were not unshared correctly.

Assert added to check whether an unsharing problem is met!

...

...

...

Serious bug fixed previously introduced by me in the kernel fixed: in some cases
an application with no arguments was created.

Stupid typo fixed.

Missing initialization of the trusting function (for the kernel).

Unused index (because of UNIQUE field count) dropped.

...

...

New index refObj_occurrence on refObj. It is required by rdfly and by the graph
generator to efficiently produce backward dependencies graphs.

changed default parameter values...

Comment added.

...

...

fixed bug in compute_equality_weight caused by wrong assumption on function
arguments evaluation order

Since several weeks whelp did not compile any longer. Fixed:
1. the new getter implementation by Zack does not implement yet remote
   calls. I have changed the (sample) configuration file to use an internal
   getter (maybe also speeding up the tool?)
2. the new parser implementation does not have hard-coded notation. The
   notation is now loaded from two files on disk (core_notation.moo and
   coq.moo). I have added to entries in the configuration file to hold the
   path to the two moo files.
3. Whelp needs to parse and pretty-print the alias definitions. The old
   parser and pretty-printer was removed from CVS. I have re-used the new
   pretty-printer, but no parser was available. I have reimplemented it
   (in DisambiguatePp :-). The file should probably be renamed. Moreover,
   the code implemented is very redundant with the corresponding one in
   MatitaEngine

...

(** xxx **) ==> (** xxx *)

...

Bug fixed: "cic:/dummy_i" is an invalid URI (that used to be erroneously accepted by the getter). Changed to "cic:/dummy_i.con".

A parser for aliases implemented (required by the Whelp).

CicNotationPres self-reference (misteriously accepted by ocaml!!!)

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.

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").