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

Missing check implemented: uniformity of left parameters in contravariant
position was missing from strictly_positive.

Missing check in positivity implemented: we did not check uniformity for
left parameters in contravariant position.

- too strict check on left parameters of constructors in guarded by constructors removed
- the cases Fixpont and CoFixpoint in guarded by constructors are useless code in the
  new kernel since:
    o  recursive/corecursive objects are now closed terms
    o  we do not allow (yet?) to pass co-recursive functions around
    o  we do check that the arguments of the application of a fix/cofix do not
       contain the function we are checking for GBC

AST to ASTFE completed up to a few computational (!!!) axioms.

...

0.5.3

0.5.3

some more fixes

fixed some GUI glitches

positivity check fixed

...

positivity check fixed, some subterms were erroneously skipped

universes in CicBrowser

better ranking interface

better tex/utf8 win

better cb

better UI for TeX/Unicode and terms grammar

Update.

remove bad aliases from toolbox

Universe levels fixed.