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

added too .moo files notation related statements

Turbo-undo implemented! It jumps directly to the final position after the undo.

OPTIMIZE table every 30 deletions: it should help :-)

ANALYZE TABLE ==> OPTIMIZE TABLE

- removed old parser
- reorganized module structure
this directory should now be renamed to ocaml/disambiguation/

compilation of needed modules now outputs to the log window

merged cic_notation with matita: good luck!

merged cic_notation with disambiguation: good luck!

adding library support (not ready yet)

fixed a specific case in development handling

some reorganization and some corrections

some reorganization and some corrections

some reorganization and some corrections

matitamake is integrated with matita
(but currently compiles on stdout)

fix

Added a new contrib div_and_mod and few modifs here and there.

Bad name should be an error and not just a warning.

New version of name checking.

snapshot, notably:
- started merge with cic_transformations, ATM all available matita
  scripts are parseable with test_parser fed with doc/core_notation.ma

* added group box (?)
* added break layout and partially implemented

bugfix: removed spurious section "helm_registry" from save_to generated files

added XmlAttrs attribute for specification of xml attributes directly
from cicNotationRew.ml

all interface is locked during advance/retract

fixed lock mark

some more replace facility: alt-r

fix

added find&replace facility

use dvariant for associtivity

removed drop.

New version of the library.

bugfix: "LPAREN" vs LPAREN

snapshot
- added keyword handling for notation specifying string literals
- added keywords to level2_ast_lexer

copied text is unlocked :)

matitamake stuff:
- added matitamake
- matita.basedir has no /xml (added in save_object_to_disk)
- matitadep and matitac take -I <path> to add that path to
  where includes are searched

snapshot
- revised concrete syntax
- split parsers and lexers
- removed IF and THEN magics in favour of IF/THEN/ELSE and FAIL

Added a function equations_for_goal similar to signature_of_goal.

Debugging comment removed.

Benchmark fixed. It was broken by the change in the handling of
matita.conf.xml*

added matitamake

added matita.conf.xml.sample

added .moo

now proofs have the correct type :-)

...

fix

* implemented unless

default USER_HOME to pwd

...

...

...

fix

matita.conf.xml.sample is now generated

added a flag to do the check of alredy-proved-theorem

tentative hack for the incredible DB slowdown.
I suppose we use the DB in a really uncommon way, billions of inserts and
queryes mixed, while (I suppose) the usual is a bunch of inserts and then
billions of queries. ANALYZE TABLE is called sometime to try to ameliorate this
problem.

...

Bug fixed: the left parameters of a record or inductive type were not added to
the disambiguation domain.

* added backtracking in matching code (hairy code!)

* various bug fix related to the environment returned when a match
  occurs
* first implementation of the "if" magic

A few .cvsignore here and there.