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.

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

...

...