Better label for the disambiguation errors window.

New (and much more complex) disambiguation error interface.
Errors are now categorized according to:
  1. location
  2. error message
  3. environment

More timeout added to autos here and there.

1. is_meta_closed should be applied only to terms on which a substitution
   has already been applied. Fixed here and there.
   Note: it is not possible to add a subst parameter to is_meta_closed since
   the function is declared in cic/CicUtil and it is used where the unification
   is not available (e.g. in whelp and library)
2. known (but never verified before) bug fixed: delifting should fail
   (instead of raising Uncertain) iff the local context is not meta_closed.
   The test used to be "does not contain a Meta"

till some patches

the incomplete proofs were axiomatized

some patches. still does not compile properly

Added timeouts to auto here and there.

Added timeout to autos here and there.

1. bug fixed: Unicode characters that are not mapped to TeX macros used to
   be post-fixed with a blank
2. bug fixed: the textual pretty-printer does not implement the same
   spacing politics of GtkMathView. Since that politics is very very complex
   to implement, I try a different solution: we explicitly insert a space
   where we want one. The widget does not seem to be disturbed by this.
   This way the let ... rec and match ... with constructs are now printed
   correctly and they can be read back.
3. syntax change: applicative patterns no longer require parentheses around
   them

/home/fguidi/... => ../../...

we removed about 100 match-with costruction turning them into applications

Added a couple of flags to auto

Our unification used to guess a very complex argument of an apply in
fermat_little_theorem. It does no longer, but the old behaviour seems to be
really lucky. Thus I change the .ma file.

Two lemmas that used to pass no more now pass again. Bug simply because every
tactic argument now requires less question marks :-(

Added unit to rings.

More coercions added in the algebraic hierarchy.

Up to f_algebras.

fixed the ugly button added by csc, now it is inside a buttonbar and uses the default gnome stop icon.

removed equality_retrieval

Better (and more localized) error message for sort_of_prod.

CicUniv.UniverseInconsistency is no handled correcly.

binaries/saturate no longer compiled since it does not compile any longer after
the huge refactoring of auto/paramodulation by Andrea

Demodulate and applyS moved form saturation to auto.

Major changes to auto, documented on the helm mailing list.

Minor changes.

a. uniform mangement for context and library
b. collapsing flexible terms (X args) into a single meta. Metas in
   head position give arity problems with discrimination trees.
c. Even terms with a single meta as conlcusion (e.g. elimination
   principles) get indexed.

The type of universe_of_goals has slightly changed, omitting
to pass a useless proof. A few prerr_endline have been removed.

This is only a temporary patch. The typecheker raises a
CicUniv.UniverseInconsistency that should be properly
captured and transformed into a tyepchecking error.

The function exists_a_meta has been modified to capture also
flexible arguments instead of metas.

New function pack_coercion_metasenv, used in auto after try_candidates
to clean up the metasenv (othewise application could fail).

Up to f_algebras.

1. developed up to algebras
2. some lemmas commented out because of a new bug in rewrite

Serious bug fixed: without a Lazy.force the user obtained an error comparing
two functional values.

Disambiguation errors are now compressed in a maybe better way.

Bug fixed: when trying to insert coercions after an Uncertain, a RefineFailure
was raised (instead of re-raising an Uncertain).

Potential performance improvement + better disambiguation error messages:
the delift functions used to raise Uncertain every time it failed; now it
raises Failure when the local context contains no Metas (that means that
for every future subst it will not contain new Rels).
Note: if we are working up to conversion (I do not think so), we should check
that the local context is Meta-closed, that is a weaker check.

Missing optimization implemented: before starting to analyze the disambiguation
domain we try first without interpreting any symbol. This way we can avoid
lot of refinements when the information in the uninterpreted term already
tells us that every instance will not be well typed.

- Disambiguation error exception enriched with more information
  (the same returned in case of correct disambiguation)
- The disambiguation error interface now shows the complete environment
  in which the error occurs. I am not sure if this is better or worst than
  showing only the diffs.

Bug fixed: the diff component of the exception raised when the term cannot
be disambiguated used to lack the last choice in case of the look-ahead
optimization.

EXPERIMENTAL: new interface for disambiguation errors.

[ Moreover, a dead dialog window has been removed ]

Dead dialog window removed.

Dead dialog window removed.

Disambiguation errors now carry more information (i.e. the patches to apply to
the current interpretation to re-obtain the refinement errors).

Dama is now in the night benchmarks.

Too verbose error message (probably activated by Enrico without really wanting
it) removed.

new objects for the LambdaDelta development (4th conjecture proved)

more new objects for the LambdaDelta contribution

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.