Added more typing information to remove a coercion.

Integration f_algebras declassed.
We suppose to prove everything on integration_riesz_spaces.
However, the definition or weak order unit is complex because of the sup
on sequences.

Up to absolute value

preliminary support for hbugs
added to the cicbrowser the CTRL-l binding for highlighting the URL (a-la-firefox)

Up to max (up to a bug).

We begin to play the real game: we have defined real numbers and
constructive connectives (only the disjunction for now) and we are
trying to define the max between two real numbers as the limit of a
particular cauchy sequence. Cool.

Integration_algebras.ma split into 6 different files.

Syntax changed (to be changed back) for left parameters of inductive types.

The OK button of the disambiguation errors interface now adds aliases to the
current script. However, the aliases are used only in passes 1 and 3 :-(

Bug fixed: inductive types were no longer removed from the environment during
a remove_single_obj.

New behaviour of the disambiguation error messages: errors generated without
using coercions are shown only when More is pressed.

TermAcicContent.Interpretation_not_found catched and handled correctly.

Up to integration f-algebras.

Debugging code is now controlled by the debug flag.

library = yes!

remove_obj is now much faster:
 1. the code was utterly messy, trying to remove from the DB files and
    to remove from disk #xpointer uris.
 2. LIKE substituted by =
 3. added QUICK and LOW_PRIORITY to the DELETE statement
 4. removed unuseful and unused debugging code that used to slow down every
    deletion

Level-1/LambdaDelta now compiles fine

Added target preall.opt.

GRAVE BUG IN COERCIONS FIXED: the insertion of a coercion used to introduce
applications of applications (that are forbidden and not handled properly).

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