The Abort button is now working properly. Cool.

Xavier code for killing a thread commented out for a while since it interacts badly with (labl?)Gtk.

This commit implements the Abort button for the GUI using a clever trick by Xavier Leroy.

restored is_identity instead of is_weak_identity

**** EXPERIMENTAL ****
The GUI of Matita is now thread-based.
In principle Ctr-C works unreliably.
In practice it works reasonably well.

added a subtle List.rev that makes the order of the equalities taken from the library as it used to be. In this way the applys test works, but is not clear why the other order does not produce a solution in decent time

...

auto always uses the context (even if paramodulation) to try to close goals left open by paramod

returns the right list of goals

50 steps on goal are fine for irrat2

removed only made with the DB

removed a pointless call to auto

...

added tests for paramod

...

added missing *)

restored old (r6662) behaviour

when use_only_paramod is true do not calculate the universe for applicative reasoning

2: is_identity -> is_weak_identity

fixed metaconvertibility that was completely wrong.
is_identity and is_weak_identity fixed accordingly

removed bad guard that was always false (assert false in the line above)

fixed (dasabled paramod)

renamed inference in founif that is more appropriate

is_identity -> is_weak_identity

hack to make the Pp work (sometimes)

new version of auto that is able to prove the irrationality of sqrt(2)

added tests for auto

restored the good factorization file

ported to the new reflexivity implementation

maittaprover uses another format

...

removed a useless printing

added metas local context maction: ?n[...]

solved issues regarding SQL incredible error proness

Implemented topological sorting according to the dependencies.

auto snapshot

...

More work on the translation of technicalities/setoids.ma.

One less open helps understanding the code!

More informative error message.

fixed bug regarding developments. paths given with -I are now made absolute

New bug found in disambiguation of records.
To fix the bug it is necessary to propagate the substitution computed
during the type-checking of the constructors to the types of the inductive
types. This is quite complex to do. One possibility is simply to add the
substitution to the proof status.

Initial work on setoids:
 - AST changed to make it more parametric on terms (for the Relation command)
 - functions that work on ASTs consider the constructors in alphabetical order
 - initial translation from Coq to Matita of library/technicalities/setoids.ma

Initial work on setoids:
 - AST changed to make it more parametric on terms (for the Relation command)
 - functions that work on ASTs consider the constructors in alphabetical order
 -

Added generation of dependency graph for the ocaml modules in matita/
WARNING (and happyness ...): first Ruby script added to our repository

rebuilt

Two tests used to have the same baseuri. Very bad.

added SRC parameter to makefile (the one placed in the root of a development) to specify the set of files to handle (if omitted all files reachable from the root dir of the development are used).

The precedence level is now an optional argument of the content to pres
transformation for terms.

linkonly now also links matitac

* ocaml => components
* initialization was missing

discriminate => destruct

{discriminate,injection} => destruct

injection_tac and discriminate_tac now replaced by destruct_tac

injection_tac and discriminate_tac now replaced by destruct_tac that
performs either injection or discrimination. In Coq destruct is called
"analyze equality".

Several bugs fixed in discriminate.
Discriminate now works on inductive types with any number of left or right
parameters.

Bug fixed: a number alias Num 0 now subsumes the case Num n for each n.

last fix.

using lua5.1 instead of lua50

override USER with bench

added $(USER) so that the night bench can override it (and not put garbage in MY sql tables)

fixed script to make csc happy

Bug fixed: aliases for numbers were no longer handled correctly (since 0 was
a wildcard only for symbols).

auto snapshot

snapshot of queries for auto+paramod

added notation

...

apply now uses both menv and subst to decide the fresh meta number

"21" -> "Implicit found"

added displaying of the dep graph of a development, click action still missing

added generation of the .dot version of development dependencies

Injection now clears all intermediate results introduced.
Injection code reindented.
Baseuri in injection.ma fixed.

1. bug fixed: injection now performs recursion lifting correctly
2. bug introduced: injections now behaves as id_tac when it has nothing to do

Added new target linkonly to link matita without re-compiling anything.
Useful for rapid debugging in bytecode.

last problem elegantly resolved!

removed old .cvsignore files
ready for 3.09.3 and ocaml.mk

ready for 3.09.3 and ocaml.mk

binNMU safe setting of debian/*
ready for 3.09.3 and ocaml.mk

Yet another refinement error localized.
Enrico should really learn to localize his own exceptions :-)

Debugging code deactivated.

useless files removed

exportation completed!!

removed useless file in source package

new release, binNMU safe

ok up to pc1

1. Stricter controls implemented in injection.
2. tests/injection.ma now contains a description of why the tactic sometimes
   fail and there is nothing really cute we can do with it. It also hints to
   an alternative solution implemented in Coq.

Bug fixed in injection: lifting was not performed correctly, but it worked
most of the time :-)

1. added a test for injection
2. injection now works also on inductive types with left parameters

As the test shows, there are still bugs even in the case of an inductive
case with right parameters only.

Bug fixed in pretty printing in new syntax of MutCases on inductive types
with left parameters.

Bug fixed in injection: injection can now work on inductive types that have
right parameters. It is still bugged on inductive types with left parameters.

ok up to pr3

removed contribs from nigtly bench

some fixes to the "test notturni"

problems-4 was due to trans_eq expecting an explicit named substitution.

- ok pr0 pr1 pr2
- added one problem (like problems-4)

1. Some warnings about unused warning fixed (hopefully well)
2. We now try to print the MutCase in the new syntax.
   This fails silently when the type of the constructor is not a spine of Prods
   ended by something not convertible to another Prod. It also fails providing
   reasonable information when one pattern has not enough Lambdas.

Bug fixed in injection: a missing lift bugged the tactic when the constructor
had more than one argument.
The tactic is still bugged when the inductive type has either right or left
parameters!

Possible bug fixed (similar to the previous one, but in another similar function).

Bug fixed in the guarded_by_descructors function: in some cases the context
was missing the left arguments! This is the first bug found in the kernel
after quite a long time.

Bug fixed in the guarded_by_descructors function: in some cases the context
was missing the left arguments! This is the first bug found in the kernel
after quite a long time.