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.

...

The outtype of the MutCase of the generated elimination principles are now
always dependent (to avoid the ugly compatibility code with Coq).

Bug fixed in check_sort_elimination in the case (not tested so far)
dummy = false, Prop vs Type.

Bug fixed: the generated elimination principles used to have Anonymous
binders referenced! Fixed.

...

...

aliases are now compared not only looking at the domain_item but also looking at the description

only regular files are ending in .ma are now searched

New version of the library, a bit more structured.

  Removed the old library.

built test_{lexer,parser} per default

removed dependency on gdome2-xslt

New test suite for generalize.
The last test fails because of a weakness of apply.

Some terms were processed in the wrong context.

Generalize ported to the new select up to unification.

snapshot
- added hyperlink handling on all notation literals

added variant thm flavour

added Variant theorem flavour

Replace is now working again and it is able to match the pattern up to
unification.

snapshot
- fixed priority and associativity
- code cleanup

...

Elim generalized to saturate its argument.

Elim generalized: the term to eliminate is now saturated (i.e. it is applied
to as many ? as needed to make its type become something different from a
product).

Cosmetic changes: a piece of code replaced with a pre-defined function.

dead code removed

Bug fixed: metavariables generated by the saturation in the rewrite tactic
were not declared as new goals in the output of the tactic.

it seems the sequent window is refreshed properly now

added query