Manual porting of CoRN to Matita.
The current version shows a bug in coercions to function classes.

Bug fixed: the conversion was done with the wront argument (a sort of typo).

Some hocus-pocus to avoid a common race condition (Gtk/??? code not
reentrant). I bet the "avoided" problem will surface again...

Unlocking the interface was not performed as the last action of the callback.

The RELATIONAL contrib must be compiled before the others since the others
depend on it.

My previous commit changed the regular timeout of paramodulation from
infinity to 30s. Old behaviour restored.

makefiles fixups

fguidi removed from RT in makefiles

Implemented:
 "by ... we proved ... that is equivalent to ... done"
and
 "we need to prove ... that is equivalent to ..."

auto => auto new

auto => auto new
added depth=4 to some file in order to make it pass

I do not understand at all why Enrico removed the contribs from the bench!

Sorry, bug introduced by me yesterday now fixed.
auto should be the new one even when the paramodulation flag is given.

Bugs fixed in merging of composite coercions. In particular the imperative
status was not handled properly and letins were handled inefficiently.

One auto modified in an apply since auto is no longer supposed to apply
elimination principles automatically.

added to applyS in nat/gcd.ma a timeout large enough for compilation in bytecode
mode.

1. applyS now uses its ~params
2. autoTactic.ml* is going to be deprecated.
   auto.ml* has now the expected interface (that of a tactic)
   and it is almost ready to replace autoTactic.ml

applyS now receives the same parameters that auto receives.
The parameters are not used yet.

Theorems from the library and from the context are indexed also in "unfolded"
version.

auto => auto new and other minor changes to make it compile.

auto => auto new everywhere + minor updates to make more tests pass

Comments updated with new reflections.

The two coercions sym_eq e eq_f gives BIG TROUBLES when checking composition during
qed. In particular, checking composition calls unification, that calls reductions,
that is problematic when there are a lot of lein in the context (as is it the case
with proofs generated by TPTP: see eg GRP486-1.p.ma )

More work to handle -debug properly.

Factorized "find_equalities" in demodulation_tac.

added support for short name targets

resumed ol auto

fixed all (that now uses long paths)

now the makefile for developments requires the depend file
that now has correct dependencies.

1. some "try ... with _ " removed
2. type inference of LetIn terms is now closer than the kernel
3. LetIn code fixed to add the type to the Defs in the environment
4. some typos fixed

reduced timeout to 100s

commented out are_convertible in is_identity
fixed metadataquery so that only are calculated without the DB (but are calculated)
removed is_meta_convertible left right in is_weak_identity
added extra dependencies between gcd < relevant_equations < ord to make
paramodulation happy. In the past this used to be the order used by make.
added an hack in applys.ma, since it used to work due to convertibility.

Some declarative tactics did not allow the "done" option in place
of "(id)". Fixed.

Inline command implemented.

Syntax of paramodulation parameters changed.

Fixed handling of exceptions by the worker threads: the exception is not
notified to the user and the thread exits gracefully.

Removed /home/tassi from the makefile!

Query fixed to handle the cases where 0 tests are failures or successfull.

Changed auto from implicit to option and renamed a few functions.

Regular expression fixed to allow '-' into test names.

sacerdot is now the user for the daily bench.

Crontab updated

No more benches without gc.

sequent_viewer.xml & co are now generated in /tmp if necessary!

updated to use destruct instead of disciminate/injection

Bug fixed: the script Menu was not locked as expected.

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