remove matitamake binaries on clean

added "commands_of_environment"

regenerated

moved dummy_floc from Disambiguate to DisambiguateTypes, since it is now needed by DisambiguatePp

...

...

Test fixed.

Two bugs fixed in the apply tactic:
 1. an application of a term of type t where t reduces to a product does not
    fail any longer: t is unfolded as required to produce enough products.
    E.g. apply (t: ~A) when the goal is False
 2. the apply tactic does not fail any longer when the goal is a product.
    When the head of the type of the term is flexible, the type is a product
    and the goal is a product (e.g. t: A -> ? vs A' -> B) the less instantiated
    term (i.e. t) is tried first; in case of failure (e.g. A not unifiable with
    A') t is instantiated adding one metavariable after another.

cic_textual_parser2 ==> cic_disambiguation

cic_textual_parser2 ==> cic_disambiguation

core_notation.ma ==> core_notation.moo

removed left-spacing of 2 em for '(' (useful only for debugging purposes)

- de-ALB-ing
- added a debugging item for notation

cic_textual_parser2 -> cic_disambiguation

removed debugging print

removed work-arounds for poor disambiguation, which should now be fixed with the multiple passes support ...

Added support for multiple disambiguation passes.
Actually, passes can differ in:
- whether they use library as fallback for unbound domain items or not
- whether they use multi-aliases or not
- whether they use coercions or not.
The current policy is to postpone the use of coercions as much as possible and to fallback to library only as a last resort.
Passes can be configured from matitaDisambiguator.ml.

added support for multi-aliases in disambiguation environment(s)

added use_coercions flag (imperative :-(, non re-entrant :-(((( )

Comment removed.

...

...

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