HUGE COMMIT:

1) sequent2pres merged into content2pres
2) more functions to render sequents/context/substs to content and then to
   presentation
3) new virtual class NCic.status with methods implementing pretty-printing
   functions (same interface that used to be given in NCicPp); objects of this
   class are now used REALLY ALL OVER the matita code (well, almost...)
4) NCicPp implements a concrete version of NCic.status
   (low level pretty-printer)
5) ApplyTransformation implements a concrete version of NCic.status
   (high level pretty-printer that uses notation). It also exports the boolean
   reference to deactivate the high level pretty printer in favour of the
   low level one
6) some code simplifications here and there (in particular for tactics)
7) return type of BoxPp changed to yield informations about hyperlinks;
   the information is not used yet by the interface and it is not computed
   yet (not that easy to do...)
8) other minor stuff here and there

coercion lookup now returns coercions ranked using the number of symbols matched, the more precise match first

code simplification

...

added retrieval function with weight

non uniform coercion names in sync with the TYPES talk, stil commented out...

...

...

...

Brainstorming

ops, we forgot to update the version indicator :)

- ld-html-root: ported to permanent lambda-delta url
- ld.dtd: we can specify a language encoding for the metalinguistic
annotation, moreover we export the metalinguistic classification
- the other files are modified in order to support this feature

Bugs and other stuff to do to complete the Matita 1/2 => Matita 1.0 transition.

Interface reduction; code clean up.

code simplification

Code clean up.

Dead code removed.

More code clean-up.

Useless code removed; interfaces simplified; etc.

1. reset of statuses simplified
2. NCicEnvironment.invalidate_all (that used to hide a bug in invalidation)
   removed. The semantics of the MTI is now more shacky, but this needs to be
   fixed in other ways.
3. {lexicon_,grafite_,...}status renamed into status

Some comments (new problems found).

Really A LOT of code to add close buttons to the tab labels :-(

Bug fixed (introduced in previous commit): opening multiple files requires first
the creation of the newScript to be replaced.

Implemented standard semantics of Load in MTI: loading a file when the current
one is unnamed and not modified does not open a new tab.

1. MatitaGuiTypes.gui interface streamlined
2. added new menu item to close a script
3. restored graying of "Save" menu item when the script is unnamed

Avoid duplicates in the list.

1. bug fixed: in the last commit on NCicLibrary we forgot that
   get_already_included must be transitively closed; fixed and changed
   the function name
2. added a cache to assert_ng (called ~asserted) to avoid re-asserting
   the same file twice during a single include command

1. bug in addition of universe constraints fixed: the recursive
   inclusion does not add constraints to the NCicLibrary.storage
2. since we no longer perform recursive cleaning,
   NCicEnvironment.invalidate_item is no longer recursive. This fixed
   definitely the bugs in undo/redo linked to "include"s

progress

more theory for lists

...

Useless code removed.

Dead and useless code removed.

Dead code removed.

When switching to a new script, the other parts of the interface are
now notified.

...

VERY EXPERIMENTAL:

first version of Matita as a Tabbed Document Interface.

The semantics of working on two tabs at the same time is not defined
(yet? ...)

...

Code clean-up

Large commit: refactoring of the code of the interface.

1. management of font sizes centralized in MatitaMisc according to the
   MVC paradigm
2. functionalities related to the script window moved from MatitaGui to
   MatitaScript

First steps towards a multi-document interface.

Class mathViewer got rid of. The circular dependency between
the scripts needs to be sorted out by putting matitaScript much
later in the chain. This commit temporary introduces bad type
expressions here and there.

1. Method screenshot moved to CicMathView where it belongs to.
2. the mutual dependency between MatitaScript and CicMathView/MatitaMathView
   needs to be solved differently (it used to be solved using guistuff, which
   I do not consider any longer a good solution). To be done.

With this commit, anything related to MathML vs Textual is now in
cicMathView.ml.

Useless methods removed.

1) matitaMathView.ml splitted into cicMathView.ml + matitaMathView.ml
2) interface of matitaMathView.ml and cicMathView.ml greatly simplifed
   so to avoid any reference to the textual/MathML datatypes.
3) up to the problem of taking screenshots, the file matitaMathView.ml
   is now oblivious of the difference between text and MathML. It will
   be soon possible to switch between text and MathML simply by changing
   the implementation of cicMathView.

Better typing.

Now useless type declaration removed.

This commit simplifies the interfaces of the various Widget-related .mli
files, so that the same inferfaces can be used both for the MathMl widget and
the textual widget.

Practically, it is now sufficient to switch between two implementations of
matitaMathView to change between MathML/textual.

Large commit:

1) some dead code removed
2) code of MatitaClean commented out (but still there for disambiguation and
   the like?)
3) dependencies and uris moved into dumpable_status (from other statuses
   and/or imperative code) and made functional
4) all the bugs related to recursive compilation seem to have been fixed by 3)

New version of the library. Several files still do not compile.

Some bugs fixed (and some still open) in recursive compilation of files:
 a) matitac now takes again either a list of files to be compiled or
    nothing (to compile all files in the cwd)
 b) ...

Bug fixed: a file A that includes a file B needs to be recompiled also
when B has been compiled after A.

Dead code removed.

Previous patch improved: we now use an ad-hoc wrapper for Grammar.parsable
in order to localize all Obj.magic --- related to use of Ulexing in Camlp5 ---
in GrafiteParser (as they used to be).

Debugging code removed.

Dead code removed.

BIG BUG FIXED (???): in place of using Grammar.Entry.parse we should have
used from the beginning Grammar.Entry.parse_parsable in order to avoid token
loss (because of backtracking) between consecutive reads. I have fixed the issue
for statements only (since they are the one that show the problem). Should I
do the same everywhere?

Backporting from new Matita:

Patch to avoid double creation of metavariables changed to a simpler one
that keeps disambiguating twice the term. The old patch introduced a few
bugs that were difficult to fix.

Notation for - (clear).

Big change:
 - new command "include alias" to include only the aliases
 - "include" now always includes the aliases and it includes everything else
   only if the file has not been already included

New syntax -H1 .. Hn for clear

Patch to avoid double creation of metavariables changed to a simpler one
that keeps disambiguating twice the term. The old patch introduced a few
bugs that were difficult to fix.

exp and factorial

some progress

Semantics of try changed (fixed) when applied to multiple goals that can now
fail independently.

Back-portin from new Matita: semantics of ntry changed (fixed?) when applied
to multiple goals.

Back-porting from new Matita: improvement to inferred type.

first commit for Helena 0.8.2
autCrg: we removed the computation of the de Bruijn degree
output: we renamed some reductions to reflect the latest terminology
brgSubstitution: icm related bugfix

It is now possible to pass a ${ident x} to another previously defined
notation that expects an ${ident y}.

[ porting from CerCo's Matita ]
1. new implementation of normalize to have a speed up in case of fully applicative terms
2. all reduction tactics used to end with instatiate that re-checked the conversion using
   unification (!!!); added a new flag ?(refine=true) to instantiate to avoid this expensive
   check when we know it is useless

Bad default for ?dorefine for instantiate

1. new implementation of normalize to have a speed up in case of fully applicative terms
2. all reduction tactics used to end with instatiate that re-checked the conversion using
   unification (!!!); added a new flag ?(refine=false) to instantiate to avoid this expensive
   check when we know it is useless

porting to new syntax

Bug fixed: propagation of left expected parameters is now working correctly also
in case of \ldots.

Bug fixed: propagation of left expected parameters is now working correctly also
in case of \ldots.

In the case type_of constructor with expected type T, T is now put in whd to
find an expected inductive type.

In the case type_of constructor with expected type T, T is now put in whd to
find an expected inductive type.

Back-porting from new Matita:

Invariant dropped: NotationPt.NCic t can now contain metas.
We do not know if the invariant was exploited somewhere...

Back-porting from new Matita:

Propagation of left expected parameters in typeof.

Back-porting from new Matita:

- GREAT: when unifying ?1 : Type[i]  with ?2: Type[j] the unifier
  randomly tried to instantiate ?1 with ?2 even when j > i, yielding to
  an unification error later on. In turn, this created that horrible
  behaviour of rewriting that failed if you did not pass enough types
  to the lemma.
- in rewriting the argument is now automatically saturated

These two fixes together allow most of the time to write simply >f as we
did in the old system.

Back-porting from new matita:

New behaviour of fo_unif: in case of  ?f args == t args'
where at least one args is flexible, it now unifies in parallel even if the
two args have different lenghts (as in the old version of Matita).

Back-porting from new Matita:

- GREAT: when unifying ?1 : Type[i]  with ?2: Type[j] the unifier
  randomly tried to instantiate ?1 with ?2 even when j > i, yielding to
  an unification error later on. In turn, this created that horrible
  behaviour of rewriting that failed if you did not pass enough types
  to the lemma.
- in rewriting the argument is now automatically saturated

These two fixes together allow most of the time to write simply >f as we
did in the old system.

Back-porting from new Matita:

Bug fixed: analysing inductive type that contains implicit used to
duplicate the metas in the metasenv since the term was disambiguated
twice, in the analyze and in the tactic that uses the analyze.

Propagation of left expected parameters in typeof.

- GREAT: when unifying ?1 : Type[i]  with ?2: Type[j] the unifier
  randomly tried to instantiate ?1 with ?2 even when j > i, yielding to
  an unification error later on. In turn, this created that horrible
  behaviour of rewriting that failed if you did not pass enough types
  to the lemma.
- in rewriting the argument is now automatically saturated

These two fixes together allow most of the time to write simply >f as we
did in the old system.

New behaviour of fo_unif: in case of  ?f args == t args'
where at least one args is flexible, it now unifies in parallel even if the
two args have different lenghts (as in the old version of Matita).

Debugging code commented out.

Debugging code commented out.

Debugging code commented out.

Small improvement: check now takes the context of the first focused
goal, if any.

Some arithmetics.

- lddl html pages: the transition to xhtml 1.1 + css 2 is complete
- helena: we made a 88 x 32 label for the Web

Implementation of proof irrelevance finished.

Debugging disabled

- auto now uses the equality of the new library

- dead code removed

- number notation ported to new library
- code for number notation made less general by hard-coding the only
  notation

Number notation ported to new library.

Invariant dropped: NotationPt.NCic t can now contain metas.
We do not know if the invariant was exploited somewhere...

Bug fixed: analysing inductive type that contains implicit used to
duplicate the metas in the metasenv since the term was disambiguated
twice, in the analyze and in the tactic that uses the analyze.