...

...

- exported CPS iterator visit_magic
- added CPS iterator vivist_variable
- added freshen_term/freshen_obj which freshen instance numbers on ASTs

Filled pre-generated notation levels with productions on dummy tokens (never generated by the lexer). This hack works around a bug in camlp4 which on delete_rule remove an entire precedence level if it gets empty after the delete_rule invocation.

done some items

commented Record type constructor

An old note (that goes back to July) integrated in matita.txt.

the case Appl Meta vs t was not executed in case t was a Constant,Mutcase,Cofix,Fix,.... (I guess only if it was a Rel/Meta).

workaround for sequent viewer flickering

added left/right

...

removed some debugging prints

items related to lazy parsing

implemented lazy disambiguation of tactics arguments, when those
arguments have to be parsed in contexts extracted by a pattern

added set_metasenv on proof_status

- uses runtime base dir to reference logo with qed
- removed some dead code

removed some dead code

tests changing under a binder

uses Map.equal to compare universes

completed test

Unsharing bugs fixed.

Unsharing bug due to a very stupid typo fixed.

...

bugfix: avoid losing attributes on boxes which have a single children
this used to cause impossibility of selecting a let .. in term

removed dead code

added {get,set}_attr

added {get,set,pp}_attr

uses \def symbol for definitions in context

done 1 item

updated

misc fixes in cic browser queries (pretty printing, url bar, ...)

added dirty hack to blacklist mult_n_2, which causes troubles... :-(

...

...

...

Refiner substituted with the type-checker in a case that is known to be already
well-typed.

...

New bug exposed.

...

Dead code/files removed.

removed debugging prints and better sample

added <include href="foo/bar/baz.xml" /> support

Bug fixed: the small logo was searched in the wrong path.

Serious bug fixed: unsharing was not performed over sequents.

Dead code removed.

Added aliases and notation.

...

Unfold tactic generalized to perform zeta-reduction.
WARNING: the tactic is bugged since it tries to zeta-expand a term that lives
in the context of the goal, not in the context of the pattern!

locate_in_* functions generalized to handle equalities in a context.
Usually only the context length is used (to compute some lifting factor).

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.