- bugfix: eta abstractions ignores attributed node while counting lambdas
- permit pattern matching on attributed asts (since attributes are transparent to pattern matching)
- wrapped with assert false some unsafe function invocations (e.g. List.map2)
- removed reset_href (no longer needed)

more refere to bindings in env type definition

fixed matitadep: now it should consider ALL depndencies

added a minimal parser to extract informations relevant to dependencies calculation

...

all initialization code is now in the new matitaInit.ml module.

matitadep now parses notation.

development windows now avoids doing an anction selecting no developments

* Obsolete debugging comments removed
* Debugging comments by Andrea marked with "Andrea:"

Notation for "ex" introduced. It is the same as the notation for forall,
but it uses \exists.

NOTE: there is a bug now in cic_notation. The notation for ex is parsed, but
it is not pretty-printed correctly!

...

More profiling code.

Great speed-up in alias_diff (about 3x).
NOTE: alias_diff is still quite slow (e.g. 2.4s in the processing of
factorization.ma). This function really deserves to be got rid of.
(Moreover, this is possible and not that difficult)

A bit of profiling functions added here and there.

Spurious interpretation removed.

Profiling disabled.

...

This commit (partially) removes a big source of inefficiency (at least for
the select function and the rewrite tactic): CicUnification.UnificationFailure
exceptions were enriched producing (in a very expensive way) a nice error
message. However, the expensive error message is useful only when it must be
shown to the user. Very often this is not the case. Thus I am now postponing
the production of the error message, changing the type of the exception.
NOTE: this kind of improvement can be applied everywhere in the code!
At least it should be applied to functions that can normally fail (e.g.
unification, refinement, convertibility, type checking, etc.)

added list.ma

- avoid catching top level exceptions when the relevant setting in the registry is set
- removed some ancient debugging prints

splitted command line arguments among debugging and non-debugging so that when BuildTimeConf.debug is false the -debug flag is not available

- added support for -debug, which avoid catching top level exceptions (still useless until we find a way to let the program die on uncaught exceptions raised by gtk callbacks)
- enable whelp syntax on command line
- uses Arg for command line parsing

- bugfix: when backtracking restore the appropriate matched terms instead of keeping the current ones
- changed column order while matching constructors, this should speed up the matching since often application head discriminate if a row can be applied or not

Removed final question marks from {apply|elim|rewrite}s.
(This used to change the goals order, but it has now been fixed by Gares)

Some code that used to avoid a fixed bug removed.

...

.ma inclusions corrected/minimized

Profiling code commented out.

CicUtil.profile made even more polymorphic.

added a function to reorder the metasenv.

...

...

added notation for: nleq, ngeq, nless, and ngtr

added notation for nleq, nlgt, ...

added entites/overrides for leq, geq, nleq, ngeq, to

re-generated

uses Hashtbl.replace instead of Hashtbl.add so that:
1) extra-entities.xml could be used to override undesired bindings
2) only used mapping are kept in memory at run-time

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.

"bool.ma" is now always included before "logic.ma", in order to speed up
parsing.

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.