Major reordering of theorems in the appropriate files.

In case of coercion to Prod, the error message shown is that _after_ the
coercion. In case of multiple coercions, only one error is shown.

fixed script

Precedence level of \downarrow changed to match that of the binary one.

snapshot

...

formal_map now defined

Definition of formal_topologies.

...

...

...

...

new directory for the newGeneration refiner

BTop is a category.

old bug in mtime computation fixed

...

1) as usual, I took the reverse notation for composition.
   "fixed" according to the internatinal tradition
2) partial proof that basic_topologies form a category

helm mailing list moved to cs.unibo.it

we skip discharging on matita opbjects (they don't have exp. variables)

cicDischarge, Procedural: we improved debugging and added some time stamps
librarian.ml: new algorithm for sorting sources according to compilation order

reverted auto experiment

AGAIN A TEST

COMMIT TO JUST RUN A BENCH, SHOULD BE REVERTED ASAP (auto run after every tactic)

Reordering of lemmas in proper places.

Concrete spaces do form a category, after all :-)

some work to make tries "printable", fixed comparison of constants in
paramodulation, added (but commented) a call to auto after every tactic
invocation to test it on the whole library.

Getting closer thanks to more technical arrangements.

...

...

Concrete spaces now defined.

Case c1 t1 vs c2 t2 where c1 and c2 are not splitted and t1 and t2
are rigid was not handled correctly. Fixed.

cicDischarge: we still have some problems here. Some fixes
cicTypeChecker: added some debug prints (commented for now)
applyTransformation.ml: improved error detection

we always save the discharged object for future reference

we have to remove the Num directory :)

transcript: we now check for non-existing objects
procedural/Coq: we now generate from ufficial 8.0pl2
                that does not have the Num directory

...

unification+pullback fix. It used to saturate a coercion (generating new metas)
but not do any unification steps on them nor using them to build a new term,
thus they were left in the metasenv with no chance to be closed by subsequent
calls to unification. The meets function has been specialized takin in input a
boolean for every direction (left/right) to state if the graph can grow in this
direction and it returns saturated coercions and augmented metasenv only for
the requested directions. Still unclear to me what does it mean to search a non
triangular pullback with a boolean set to false....

transcript: improved debuugging facilities
orocedural/Coq: we escaped the non-ASCII7 characters

...

we forgot to delete the old CoRN mma files :)

transcript: we improved the parser/lexer to read the scripts of the standard
            library of coq. Coercion extraction is disabled for now.
contribs/procedural: new root for mma files generated by transcript.
                     We now have the mma files of the cic:/Coq/* objects

fixed case of divergence

fixed notation

restored

....

...

...

removed debug pps

comparison function fixed

...

removed old non-working file

notation_id were compared using Pervasives.equal this was rarely triggering the
exception eq_on_functional_values. New implementation of compare using
a camlp5, that only provides an equality function, that is hacked to
return an integer.

stop running LAMBDA-TYPES as a test, can be reactivated when it will take
less than one night

hbox => hvbox in constructor arguments in match patterns.

Setoids are now more pervasive.

Uri ending in '' were not accepted. Fixed.

new debugging option

Relations are now closer to Sambin's ones. I.e. they range over Types
and not (sub)sets.

...

...

new baseuri for procedural CoRN
to follow the discharge name convention adopted in applyTransformation

applyTransformation: variable discharging in procedural/declarative script
                     reconstruction is now activated
we rebuilt the dependence files

cicDischarge: new module for discharging the explicit variables occurring in a
              CiC object. This is used in the procedural/declarative
      reconstruction of Coq's library (es Coq/CoRN devels)
cicUniv: we add a default_ugraph set for now to oblivio_ugraph
acic_procedural: improved error handling
depend, depend.opt: we updated some

Convergence is now defined.

Better notation, in particular for subset comprehension.

Notation |.| moved to core_notation.

fixed some stuff

bug fix in inline syntax

...

New categories REL and BP.
Nice naive infrastructure for setoid rewriting.

New cool "type-checking" notation using colors and non-linear patterns.
Still not working propertly for and and for-all elimination.

Do not mess with my window manager: the Cic Browsers are no longer slaves to
the main window.

Non-linear patterns are now allowed in notations.

transcript: bug fix in the generation of axioms
            variables are now unexported
CoRN-Procedural: regenerated and Makefile improved

...

Procedural: bug fix in comment generation
applyTransformation: now mma compilation fails on procedural generation errors
matitacLib: when the mma fails the generated ma is removed

...

...

Definition of categories.
Proof that basic pairs form a category.

Some notation moved to core_notation.
A few new things in datatypes/subsets and related stuff.

Also create the graphviz graph.

New debug item to print aliases.

Procedural: explicit flavour specification for constants is now working
            procedural inlining of inductive types is now working
    fixup in the generation of comments
grafiteAstPp: syntax fixup
transcript: now generates explicit flavour for inlined constants
            so we distinguish between definitions and theorems :)
    [the attributes are not present when we inline from Coq's library]
CoRN-Procedural: mma files regenerated with explicit flavours

notation with mstyle attributes, like colors and size

...

pango escape fixed

...

Avoid warning.

Added catching of an exception to implement a missing occur check:
when unifying ?1 : T with t : T', T and T' are unified first. If ?1
occurs in T', it is moved from the metasenv to the subst, and the
exception here used to escape.

svn:ignore property is now swr correctly`

basic support for imposed flavour in procedural object rendering

escape < in pango attrs

added support for font scaling to autogui

added interpretation for \naturals, \rationals, and \integers

Fixed two legacy comments

fixed recursiveness check

fixed recursiveness check

fixed check, if 0 constructors then no List.nth is allowed

allowed sort elim now check for recursive types

fixed allowed sort elim