...

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

s/debian\//debian/: avoid issue on make dist with new automake

bumped version to 0.0.7

enable static binding of C/OCaml glue code

another bug of auto

...

$ matita filename
if filename is non-existent then creates it

added test for elim

tab -> spaces

alim of now resets the counter

...

matitaclean now removes the .moo file, if existent.

env creation fix

Bug fixed: no .moo can be generated if the status is <> No_proof

Debugging message removed.

now tables are recreated if needed and mattiaclean all really clears the owner env (purging tables that will be recreated by matita/c)

notify was not called when Margin was raised. Fixed.

tables for matita.owner are created at boot

fixed according to the new fresh name generator

matita.ma.templ must be symbolically linked

fixed a problem when newScript was called
(the filename was not resetted properly)

removed gdom2 dep

- bugfix: correctly handle real "index.theory"
- removed some debugging prints

Bug fixed: "intros n" should fail when there are less than n products or
let-ins. In particular "intro" should fail if the goal is not a product or
a let-in.

added index.theory handling

Fixed a bug in the "do" tactical that made it diverge.

mk_fresh_name now returns [name] instead of its basename if [name] is unused
in the context

no longer handle Shell exceptions (no more used by helm-getter)

added backtick function

no longer uses Shell library

- updated META dependencies (no more dbm, no more shell)
- removed module Http_getter_map

uses mowgli's getter conffile as sample

some more tests

reimplemented on top of latest getter library (no more maps!!!!)

bugfix: leave ".theory" suffix in place for theory uris

help string in sync with available commands

- handle prefixes on the same line in conffile
- cosmetic changes in settings pretty printing

check on baseuri

added tests for contructor and clearbody

1. tactical "try_tacticals" renamed to "first"
2. tacticals are now implemented as a functor to abstract the type of
   the tactic
3. tacticals are now activated in matita. Their arguments are parsed in the
   right context.

clean did not remove matitatop*

added test for change

added test for assumption

clear now fails if the hypothesys doesnt exist, and doesn not typecheck
the whole context

added support for multiple binding of the same prefix (needed by the
getter daemon for handling stylesheets)

fix

added script template
added test for absurd

do not .body/.types/.proof_tree files from ls output

- bugfix in cache handling for remote resources
- more informative Resource_not_found exception (include method's name)
- catch http error exceptions

now it doesn't try to apply a cleared hypothesis

better exception handling for HTTP errors

* Bug fixed: "tac." was parsed as Seq [tac]
* Pretty printing of Seq and other tacticals was utterly wrong.