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

reordering of lexicon status partially avoided to make it sure
that interpretations are not moved around. I still argue that an alias can be
removed from the back of an interpretation, no idea how this would interfere with CSC recent patch

transformation from automath to intermediate language started

Dedekind sigma completeness for the natural numbers.

typo

some notation added with a bit PITA

final relevance check

copyright information added in the grundlagen text

when -debug do not catch

when -debug do not catch

replace assert false with AssertFailure

Initial version of the Helena Checker
- For now just parses an automath book (automath grammar by F. Wiedijg)
  the grundlagen is provided as (the only existing) example
- In the future will convert an automath book to a lambda-delta environment
  several lambda-delta extensions will be supported

New lemma
theorem eq_p_ord_q_O: ∀p,n,q. p_ord n p = pair ? ? q O → n=O ∧ q=O.

more notation

...

print the name not found in the env

Testing some performance tricks by caching the list of the first n primes and
showing that they are good either with nth_prime (sloooooooooowww) or with
sieve (slooooow and not proved correct yet). With sieve we are currently able
to verify the list of the first 103 primes in a sort of reasonable time.
The 103rd prime is only 593 :-(

better names in a lemma to increase readability