This commit was manufactured by cvs2svn to create tag 'pre_notation'.

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

added some items

fixed url

...

version 0.7.1

The fix and cofix cases of the select were not finished. Done.

1. PrimitiveTactics.new_metasenv_for_apply changed a little bit, moved to
   ProofEngineHelpers and renamed to saturate_term. It can be used to
   fully apply a term to metavariables until its type becomes different from
   a product.
2. the tactic rewrite now saturates the user provided term
3. the select function (to map a pattern to a set of physical pointers) now
   work up to unification

WARNING: replace and generalize will not be working for a few hours

An impossible case changed to an assert false.

...

added some other items

added some todo items

...

...

1. Warnings are now printed in orange (yellow was unvisible on a white
   background!)
2. the "Bad name" error is now a "Bad name" warning

apply_tac now catches TypeChecerFailure and raises Failure

fixed auto when the context has some deleted hypothesis

No more need for symbolic links: .matita, the configuration file, etc. are
now looked for in the directory ./configure was launched in.

Bug fixed: uris can contain '-' (e.g. cic:/Sophia-Antipolis/...)

Names bound in lambdas can now be used in the "canonical" name of the theorem.

Check function for Matita name convention.

Raising an error on a bad theorem name.

- new upstream release
- gcc 4 abi transition