First commit with new (incomplete) disambiguation engine.

sottotermini e confluenza (manca pr_substs).

we started the implementation of higher order saturated sets

- rc_sat.ma: we changed the notation for extensional equality. we now
use \cong like in geometry
- rc_eval.ma (second part of former rc_ma): we completed the evaluation
by adding a stack, and we proved weakening and thinning for it

- notation is now in a separate file
- sn.ma: we updated the axiomatization of SN while correcting the saturation
conditions
- rc_sat.ma: we proved that depRC is a candidate

- new file ext.ma with the objects needed for the normalization so
far, that should be removed or should go into other files
- sn.ma: we parametrized the saturation conditions
- rc_sat.ma (first part of former rc.ma): we introduced extensional
equality on candidates

we started to set up the strong normalization proof.
we plan to use saturated subsets of strongly normalizing terms
(see for instance D. Cescutti 2001, but a better citation is required)
rather than reducibility candidates.
The benefit is that reduction is not needed to define such subsets.
Also, this approach was never tried on a system with dependent types.

fork for Matita version B

we added some comments

Added typing rule for dummies

Added lambda

enabling destruct defs

Hyperlinks are back.

Hyperlinks are now computed correctly. I least I hope...

Removed inclusion of logic/equality.ma in datatypes/list.ma (not needed and
source of conflicts in other scripts).

Bugfix for elimination principles.

Bug fix for generation of elimination principles.

Added some typing info to elimination principles, allowing the refiner
to succeed in more cases, also speeding up the generation process (no
more slow record definitions).

Added some typing info to elimination principles, allowing the refiner
to succeed in more cases, also speeding up the generation process (no
more slow record definitions).

The sequent window now always scroll to the bottom when its content changes.

Bug fixed: the script windows did not scroll correctly because I used the
wrong method.

ctrl+pgUp/Down to navigate tabs

ctrl+pgUp/Down to navigate tabs

...

Bug fixed: the newScript method must be called only after registering the
gui. I have moved the invocation of self#newScript from the initializer to the
instance() function to solve the issue (an ugly gtk error when Matita starts).

Bug fixed: the accelerators for Close and Quit were both Ctrl+q (???)

Last commit reverted (it was an error).

Part of last HUGE COMMIT about NCic.status

Stupid bug fixed (introduced a couple of commits ago): the close button for
tabs always closed the first tab instead of the right one.

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