...

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.

fix please

matita now asks to save .moo if possible or cleans the dust the
execution has produced

added docu comment

typo fixed: s/msemantics/semantics/

removed (wrong) output encoding iso-8859-1

Shell variables are all global! Fixed a bug that prevented the removal
of the temporary directory after the end of the text.

-rectypes missing for native code compilation

Some precisations on a few comments by Ferruccio.

snapshot
- bugfixes here and there ...
- precedence still need to be fixed

name specifications added for elim_intros, elim_intros_simpl and elim_type

Debugging back to false

Wrong merge repaired.

matitatop now cleans all before exiting in every situation.
Indeed, quite often it cleans all twice :-)

Another "hard" test that used to fail.

Bug fixed: the outtype of a match when omitted was interpreted as an implicit
type (instead it is an implicit term). Thus its type was restricted to be a
sort.

function to domp moo_content is now exported

This commit fixes matitatop that was no longer working without arguments.
It also make matitatop clean everything without exiting, unless the user
types ^D in the ocaml toploop :-(

now the moo contains also composed coercions (and It should prevent
the .moo user to recreate them)

* new interface matitaTypes.mli
* when exiting with an error message matitac cleans what it produced during
  the interrupted compilation

let's find the .ma files also in subdirectories

snapshot
- preliminary support for MathML markup generation

tests/* ==> *

Gtk loop was called only when a proof was terminated. Now it is called after
every line.

id ;-) and lapply patched

Ported to separate compilation and the new getter implementation.

added mark moving refresh

Baseuri changed to move replace into matita.

re-added $(H) to matitaclean

Fixed a bug that prevented the removal of the XML files during the
./matitaclean all

baseuri changed to move the test into the matita namespace