factorization.ma

New version of the library. nth_prime, gcd, log.

Bug fixed: when several instances are tried during disambiguation, do not add
aliases unless they are absolutely necessary. Even in this case they should
be one-shot aliases (not implemented yet).

Enabling/disabling profiling is now controlled by a boolean (and not by a
comment!!!)

we have to pass back lastmeta and not newmeta (newmeta <= lastmeta).
just a cut and paste bug...

valid baseuri in template

no longer use absolute path for naming notebook labels

fixed parsing of --x=x ("'uminus" is now right associative)

New policy for the disambiguation passes.

useless alias removed

removed a comment/bug report about let..in rendering, now fixed

fixed "let .. in" rendering, adding the break between the "in" and what follows

- changed moo representation in MatitaTypes.status, no longer a string list, but a command (in AST format) list
- fixed redundancy in moo: aliases, interpretation, and default commands are always present only once in a single moo
- added MatitaTypes.add_moo_content: from now on it must be then only function used to add content to moo objects

cosmetic changes

fixed dummy_floc

- fixed dummy_floc (now in DisambiguateTypes)
- cosmetic changes

added moo dumping debug item

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.