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

some more work

more work on q

some more work

better, reparsable, notation

removed <_,_> notation second interpretation for dependent pair, since it used
to have an exponential slowdown on refinement of huge terms....

notation factored, coercion commant taking terms and not only URI

missing file added

metaAut.xlate_item started

we set the http daemon timeout to 15 minutes, which is the default timeout of   wget, because some proof terms are processed in more than 5 minutes.

more work, but russell too slow

add \\ in front of tex macros

notation support fixed to parentesize in a more sane way and
andded two windows:
1) tex/utf8 table
2) terms grammar

stylesheet application moved after header send

xxx

- grafiteParser.ml: the callback invocation was displaced
- cicNotationPres.ml: hack to have more brackets because
  (forall .. \to ..) was rendered without brackets. FIXME!
- LAMBDA-TYPES: improved Makefile

left -> right

Fixed bugs in the documentation of notation.
All TODOs left I do not know how to fill.

More documentation for notation.

Further documentation for notation.

- partial implementation of pattern for case documented
- notation partially documented
- omitting the precedence level in a notation declaration is no longer allowed

fixed core notation

notation fixed to be NON associative by default

1. bug fixed in generalize_pattern: a lazy const_tac should have been
   relocated. The interesting case is

   generalize in match a in \vdash %

   where a occurs in the goal under at least one binder

2. pattern for cases partially implemented. It is now possible to perform
   a case on the hypotheses as long as the conclusion and hypothesis patterns
   are trivial (i.e. %)

- notation fixed according to the new stricter semantics
- generalize no longer required before case

- Procedural: we now check that an eliminator opens as many goals as the                      constructors of the eliminated type
              So nat_double_ind is not an eliminator for Nat :)
- Base-2    : now compiles correctly because we fixed the preamble :)

notation on steroids: 'term 40 x' is a valid variable name in notation and
places 'x' at term level 40 even if the notation is placed elsewhere

interpretation documented

initial support for notation that specifies the precedence of term variables, that allows to omit many useless parenthesis

removed unused variable

some work on Q

general reorganization and first (unconditional) proof of lebesgue over naturals