- addded unicode_of_tex
- added \neq macro

Paramodulation initialized.

...

added optional "paramodulation" parameter to auto to turn on paramodulation

added optional "paramodulation" parameter to auto to turn on paramodulation

- better exception handling
- compiled with -pack to get a Paramodulation namespace
- fixed a bug in Inference.unification_simple

When matita is started on a non-existent file, it avoids creating it
immediately!

Original semantics of a now almost random piece of code restored.
Fixes the automatic compilation of .moos when matita is started from a directory
that is not the root of a library.

An object should be removed from disk (i.e. from the Getter scope) _before_ removing it
from the environment.

CicEnvironment.remove did not remove the object from the unchecked_list.

fix

Removed debugging print.

matitaclean all now destroys the .matita/xml directory

Big changes:
 1. the .moo files are now kept in the logical structure (i.e. in .matita/xml/*)
 2. matitaclean is now able to correctly remove all the .moo files
 3. the compilation target in library and tests is now foo.mo (it used to be
    foo.moo) and it is PHONY

add_obj is ATOMIC

some prerr to better understand the mkdir -p error

added env content debug print

...

added some typechecks to avoid using equations with the wrong type

dependencies

removed .depend from .cvsignore

added some typechecks to avoid using equations with the wrong type

added CicNotation.load_notation call to disambiguate terms

if paramodulation fails, go on with the normal auto...

Bug fixed: LICENSE and AUTHORS were searched in the current dir :-(

...

Regression fixed: goto used to stop (again!) to the new cursor position when
the user clicks somewhere. The source of the regression was the difficulty of
remembering the position of the marks while the text is modified (by automatic
insertion of aliases). Solved by using ad-hoc temporary marks in place of
iterators (first version tried) and offsets (most recent version tried).

...

...

...

S_pred moved from Z/times.ma to nat/orders.ma

MatitaSync.remove must remove the objects also from the environment.
This fixes the following bug: in matita open a file B that depends on A
(that gets loaded in the environment); then switch to A without exiting
matita. It is now impossible to re-compile A.

removed old broken code

integration with paramodulation

integration with paramodulation

modifications/fixes for the integration with auto

entry point of the stand-alone saturate

added paramodulation package

Comment "comments" removed from the outbox :-)

Better tooltips.

Tooltip removed.

...

View tactics bar ==> Show tactics bar

...

After a goto the focus is now grabbed back by the insertion window.

Debugging code commented out.

Debugging code commented out.

According to the Gnome Interface Guidelines the Help menu must be aliged
as the other ones. It should not be all alone on the very right of the screen.

...

New files AUTHORS and LICENSE.
New about dialog box (automatically generated according to the Gnome Interface
Guidelines). The dialog box is filled with the informations from AUTHORS and
LICENSE.

Empty Box.Text changed to Box.smallskip.

Several interface improvements here and there.
The interface is now closer to the Gnome Interface Guidelines.

better handling of backgroud compiler process

New target cleantests.

Pretty printing of the disambiguation environment no longer ends in \n.

Nicer handling of automatic text insertion.

A "\n" is now prepended to the aliases that are inserted (to avoid the
creation of horrible long lines).

Bug fixed: we used to use iterators on a text that was modified, making
Gtk raise non-critical erros.

fixed typo in 'leq interpretation uri which enable nice rendering of
coq's le predicate

...

...

Undo/Redo in the popup menu are now working correctly.

Redo fixed with a strategy similar (but not equal) to the one for undo:
1. we save the position of all the marks
2. we redo
3. we undo
4. we save the position of the cursor after the undo
5. if necessary, we restore the initial position of all the marks,
   we move the cursor to its position after the undo and then we goto
6. we redo

Assert false removed (although conceptually correct).
The problem isgenerating names during the refinement of incomplete terms;
the right solution would be to generate names only AFTER refinement.

Unuseful code removed.

...

fixed file descriptor leak

use safe_remove to remove files instead of Unix.unlink

sorted cicBrowser's listings

Bug fix: undo now respects the locked area.
Algorithm to fix the bug:
 1. save the status of all the marks
 2. undo
 3. save the status of the cursor after the undo
 4. redo
 5. restore the status of all the marks
 6. if necessary, move the cursor back to its position after the undo
    and perform a goto to unlock the area
 7. perform the undo again

The same algorithm should be applied again to the redo operation!

New menus Undo/Redo (bugged), Cut/Copy/Paste/Delete.

blocked undo of authomatic text (template)

A tab converted to spaces as it should be.

message if the duplicate check may take too long

matitac now automatically cleans a non empty baseuri

...

Ctrl^D in matitatop fixed (was broken by the new parser of Zack and Luca)

...

Missing case (Cast) implemented.

New naming scheme (by Andrea).

New naming scheme by Andrea.

patched

Bench fixed.

Used to left temporary file if something failed.

Many bugs in the Makefile fixed.
make inside library/tests now stops at the first error
make tests{,.opt} goes on trying to compile everything (for the night benchmark)

freshNamesGenerator moved into cic_proof_checking.

Moved freshNameGenerator inside cic_proof_checking (and revised).
CVS :

New naming policy for local variables.

do_tests.sh now returns with an error if one of the compilations fail

the decompose tactic is now working

avoids generating a wrong/empty/dummy depend

Bug fixed: matitaclean and matitadep now ignores every parsing errors and
simply continues. Before it used to avoid cleaning things and --- much worst ---
generating an empty .depend.

handled difference associativity for the same level of the extensible grammar
(no more "<W> changing associativity of level ..." messages)

- A few suggestions on how to solve a few bugs
- GUI bugs reordered to have the easiest first

Bug fixed: the "find" command now scrolls the window appropriately.

...

Bug fixed: clicking on a new position while advancing/retracting now
does absolutely nothing (i.e. at the very end of the execution the cursor
is at the end of the blue area).

Smart scrolling during script advancement implemented.

added generation og disambiguator META (future name of cic_textual_parser2)

- synced notation pretty printing with parsing syntax
- added pretty printing of notation patterns via `Raw attribute