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.

matitadep: we now handle the inline of an uri, we removed the -exclude option
matitaInit: we removed the -drop option (now handled automatically)
transcript: we removed the baseuri generation
CoRN-Procedural: the mma files and the depends file are now available

transcript: now we can generate procedural output
CoRN-Procedural: development started:
                 we aim at the procedural reconstruction of CoRN

...

...

In some universe, membership is a morphism.

Sambin's & Valentini's toolbox (???)

Dependencies removed.

...

frac is an infix operator!

Error message improved.

Rendering of \infrule improved.

we implemented the support for generating ma files from mma files

added notes about notation

add conf key matita.debug_menu

avoid empty hvbox

...

Semantic analysis implemented (sort of).

...

New input notation for bottom-up tree construction finished.

Snapshot.

Input notation.

better metavariable context

metavariable context has a separator now

exception inside regex callback not re-raised if equal to sys.break

Bugs fixed:
\frac is an infix operator
\infrule is a prefix operator

1 => \\e

Executables are now ignored.

Procedural: some comments added in the generated script
tests/fguidi.ma: we removed the dependence from legacy/coq.ma
ApplyTransformation: new function procedural_text_of_cic_term
                     for use in matitaScript (still disabled)

notations for lists adds some breaking points

Duplicated doc removed.

Snapshot (not working).

a) update with upstream version
b) new: implemented semantic analyzer from untyped to typed AST for
   an imperative structured function-less C compiler
c) all URIs removed from .ma files

cic2acic: new function acic_term_of_cic_term
matita/Makefile: LAMBDA-TYPES tested only in opt mode

more notation moved to core notation, unification of duplicated CProp connectives

Since CProp_i = Type_i everything lowered without 2 distinct Sigma.

CProp_i <= Type_i , Type_i <= CProp_i

models over N fixed

new q_function representation

removed dummy comment

Using Prop conjuction on Props lowers the universes.
SigT instead of ExT

lambda-delta: we added the support for position indexes in global references
              we added a pretty printer for the intermediate language
librarian   : utime stamps now appear only in debug mode

Procedural: we added the support for rendering definitions and axioms

Procedural: we added the support for theorem flavours and we fixed the handling             of unexpected proof constructions

cicUtil            : we added a context to is_sober to check for consistancy
                     of RELS (not implemented yet)
doubleTypeInference: the inferred name of an anonymous lambda must be the name
                     of the expected prod :)
acic2Procedural    : we added a consistancy check that was missing

Procedural: bug fix in the procedural rendering of the abstraction

librarian: retrieval of buildable files speeded up a lot
Procedural: some bug fixes
termContentPres.ml: syntax of let-in construction fixed
LAMBDA-TYPES: some improvements in the Makefile

New feature/bug fixed (hopefully): it is now possible to use fixed (term)
variables in fold bodies.
The notation for exists is now fully working as expected.

Notation for existential partially fixed: it is now possible to write
\exists a,b,c:T.P
(possibly omitting the type).
In any case, however, the type is got rid of during parsing.

A very nice experiment using notation: we define the notation for natural
language derivations so that, when looking at the proof, we see it as a
natural deduction tree! Useful to teach logic to first year students, but
much work still need to be done (expecially to give derivation trees to
the system in some way).

Exists is no longer an ad-hoc notation hard-coded in the parser.
It was so becauses it was previously impossible to declare a notation that
changed the level of its subterms.

Added new ternary layout \infrule premises conclusion name.
Very useful to render proof terms as trees.

value has a specification

updated changelog

more work on dama

fixed regression in casting an argument to funclass, this incidentally leaded to a single look_for_coercion_function

some bug fixes

better notation

minor fixes

CProp hierarchy fixed:
- CProp universes are not swept away
- CProp i : Type j (where i < j, used to be a fresh j)
- new kernel universe inconsistency error message improved
- pp function for universes constraints for new kernel

Formal topology example fixed to eploit left parameters to reduce the universe
height and solve universe inconsistency

tab -> '        '

...

simplified coercDb implementation with additional info about the position of
the coerced argument. Now (C ??? x ??? y z) is printed as (x y z) when C is a
coercion and ? are implicits or saturations generated to apply the coercion to
x.

New case in unification, when there is a triangular pullback and the
coerced is not flexible an unfolding of the composed coercion is attempted.
this helps in the case:

  C ??? X ??? y ? +?+ C1 ??? (C2 ??? X ???) ??? y z

where C = C1 composed C2 but X is rigid abd conversion fails cause
x != ? and the heads are different... unfolding C helps