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

* safe_remove exported and moved to MatitaMisc
* safe_remove used to remove the files from disk

ported to new getter interface

bumped license year

new getter implementation: no more DBM maps

handle Not_found exception in extension

notification of changes is now done only at the very end of the four
main actions: goto, reset, advance and retract.

icons added to the list of required symbolic links

make clean now prints what is being removed

default

"input" was meant to be "include"

New command   default "foo" uri1 ... urin
to set uri1 ... urin as the default foo.

Actually it can be used to set the current equality, true, false and absurd
like this:

default "equality" equri sym_equri transeq_uri eq_induri eq_ind_ruri.
default "true" trueuri.
default "false" falseuri.
default "absurd" absurduri.

New command   default "foo" uri1 ... urin
to set uri1 ... urin as the default foo.

Actually it can be used to set the current equality, true, false and absurd
like this:

default "equality" equri sym_equri transeq_uri eq_induri eq_ind_ruri.
default "true" trueuri.
default "false" falseuri.
default "absurd" absurduri.

pretty printing of URIs

aded confirmation dialog for baseuri redefinement

moo do not depend on .depend

center on parent now works for ask_confirmation dialog

All the tactics have been ported to use the objects in LibraryObjects.

include

Comestic changes.

coercions are now stored in the .moo file.

Cosmetic changes.

New function (only partially implemented) to pretty print an Ast at the
semantics level.

added some utility functions on filename suffixes

Use eval_from_stream in place of eval_from_stream_ref to avoid printing the
prompt.

include must not add aliases in the script!

"include" command implemented.

"include" command implemented.

matitaclean splitted in matitacleanLib and matitaclean.

alias declarations are now put in the .moo file.

matitaclean now call getter.ls using a buri with a trailing /

Improvements in matitatop: instead of doing exit -1 it enters the toploop
after a ^C.

Equality tactics are now used in the first half of the script.

Note: it seems that "elim H ?" is more powerful than "rewrite < H ?" since
it is able to discover the value of the implicit argument ?. To be improved.

The equality tactics are now exploited.

All the equalityTactics have now been ported to use both the equality of
Coq and that of Matita.

Note: the only problematic tactic is replace that must pick an equality without
any hint. Right now it always picks the one of matita.

New theorem: eq_ind_r.

cosmetic change: a space removed (to make tests/Makefile and library/Makefile
the same)

fixed bug in proof generation, new weight function to sort equalities, which
gives a huge speedup

may fix the nigtly build

more makefile work

make tests and make tests.opt now call their counterparts in library and tests

The tests are now in alphabetical order.

match.ma removed

* match.ma removed (it is now splitted in several files in library/*.ma)
* Makefile.tests removed (redundant with tests/Makefile)
* make tests and make tests.opt now call the same targets in library and tests

...

conflicting baseuri

matitaclean is necessary!
However, we need a fast ls method for this. Waiting for Zack's new getter...

...

* makefile improved
* new target-schema: *.opt

new targets:
  opt
  verbose.opt

...

New argument: the cleaner.

make all is now nicer

Two targets now:
 make all
 make verbose

make MATITAC="../scripts/do_tests.sh ../matitac /dev/null"
can now be used to benchmark the output

...

Makefile improved

The library of matita is borned! Long life to the library of matita.

ma -> moo in dependencies

more logging information on received request

uses relative OCAMLPATH

now maketests uses matitaclean (but not in the right way)
tests are made in the stupid order, not in the needed one

first snapshot of separate compilation

on is now a keyword (needed in let rec)