Yet another implementation of the single aliases / multi aliases idea.
The new implementation is much simpler: single aliases are used everywhere
in the disambiguation phase; however, when a term needs to be looked for in
the library, it can be looked in a user-provided multi aliases environment
instead.

NOTE: the new implementation fixes a bug of the previous implementation: the
most recent alias in the multi-alias set was printed last in the .moo files,
changing the performances of the system.

...

improved discriminate test: check if it works on inductive types with left parameters

bugfix in discriminate: now works also with inductive types with left parameters
discriminate code has also been re-engineered and re-formatted

added \neq notation

bugfix: save "~" backup together with the non-~ version instead of in the current dir

added -debug flag which avoid catching top-level exception (usefule for stack backtrace)

- changed command line interface of cicbrowser so that everything which could be written in the "URL" bar can be provided on the cmdline as well (even without double-quoting)
- ported to new ppmetasenv (swapped arguments)

uniformed ppmetasenv to other pp* methods: substs are now passed _before_ the metasenv

moved matita logo in the right place

bugfix: default "false" used to set the _true_ uri ...

fixed a finalization issue for connections closed twice
thanks to Erik Stroke for the patch

bugfixes:
1) ask for saving/mooing only when the user has choosen a file to load
2) opening a file doesn't call goto_top (removing all xml, even if the moo has
   been generated). This fix should enforce the invariant that a moo exists only
   if the corrsponding xml objects do.
3) the switch_page callback is inhibited before removing pages in
   sequentViewers#reset

done some items

added hyperlinks on case pattern heads and outtype

enable selections and href handling on elements having href and no xref, this
permits selecting/following links on case pattern heads and outtype

Product, pair and projections.

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.