Beginning of the development of integration algebras.

Content level representation of LetRec changed.

Content level representation of LetRec changed.

New content level representations for LetRec, Inductive and CoInductive.
For LetRec the pretty-printer is now in sync with the parser.

files with newest objects (to be included in the respective developments)

carr_of_term now returns Fun if a Prod is encountered

fixed defaultauto behaviour. not the cache is preserveed

timeout if unspecfied should be set to infinity, not 0, since the timeout inside the flagfs structure is a time in the future, not a decreasing quantity.
every loop of auto the check gettimeofday() > timeout raise Fail

The default for paramodulation is now back to false (I set it to true
by mistake).

auto => auto new.
There is still one auto left that does not work with the new implementation
(because of implicative hypothesis for local lemmas?)

Inclusion "improved".

CoRN integrated in the night benchmarks.

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.