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

- we replaced a normalize with a whd in the classification algorithm
- we turned on the display of the inner types to debug drop/props.ma

More definitions, following Ciraulo's Phd Thesis "Constructive Satisfiability".

- Procedural: bug fix in rendering the application: we must handle the
              arguments that are inferrable but do not occur in the goal
- LAMBDA-TYPES: bug fix in Makefile: MAS was not computed correctly

Compatibility finished.

Nice: cotransitivity proved.

More work.

First few lemmas. But I have some problems in making Matita accept
my constructor.

First experiment in Padua about formal topologies.

...snapshot

...

some work

svn:ignore set on LambdaDelta-2

- new tactic applyP for use in the *P*rocedural script reconstruction
- LAMBDA-TYPES: the mma files from the LambdaDelta section

Fixed a bug which prevented mutually recursive definitions of 3 or more
functions from being added to the library

...

return 1 in case of failure

0.5.2

0.5.2

...

...

...

calculation of the sort user to choose the rewriting principle fixed
(the one of the goal was used also to rewrite in an hypothesis)

- lambda-delta: some speed up (not very much :) actually)
- LAMBDA-TYPES: bug fix in Makefile

shifting done, merge attacked

shift almost done

new specification

we improved the data structures used in the translation to the intermediate
language

some more work on q

we tranlate an Automath book in an itermediate format where:
- the local references are resolved as position indexes
- the global references are disambiguated
- the parameter applications are completed
For now the trnslation is slow because the involved data structures are
inefficient

some more work to factorize out uninteresting parts of the proof...
still to close the key lemma...

more work to try to understand where the issue is

lost in the wood

more work

few more steps

more work