components/library: dotdothack removed
legacy & LAMBDA-TYPES support $(MATITAUSEROPTIONS) (= -system for fguidi)
LAMBDA-TYPES: two missing generation lemmas added

New syntax for patterns.

prodT ==> prod

A) New version.
B) set "baseuri" removed
C) minor clean-up

we added the classic substitution function

firs attempt to compile with ocamlbuild

the proof of bertrand's conjecture is now complete

I added some debugging information

added MATITAOPTIONS -onepass as for LAMBDA-TYPES

LAMBDA-TYPES: added wf3 (legal context predicate);
              Unified-Sub removed because of its early stage

$(H) added :)

LAMBDA-TYPES: dependences calculation improved

LAMBDA-TYPES:
we introduced incremental dependences build to speed up the compilation
dependences are now dynamic so the file "depends" was removed from svn

- added some options to matitadep: -stdout and -exclude
- LAMBDA-TYPES: improved Makefile, Base-2/theory.mma is no longer needed

sieve of erathostene (proof of soundness almost done)

A new very simple example for recursive functions. Still bugged, but getting
better.

Avoid translating back recursive fixes to the same URI.

Avoid application to 0 arguments.

Better handling of exceptions.

svn:ignores fixed

-onepass option removed from Makefile to comile Base-2/ext/arith.ma ???

LambdaDelta-1 regenerated as a subdevel ov LAMBDA-TYPES
some additions and redundant dependences fixed

splat_args is now better understood and debugged: we need TWO splat_args, one when
the term is a Rel (that skips the bound variables) and one when the term is a Fix
(that passes bound variables around).

added small test, fixed some bugs

many fixed in translation functions

dependences needed a fix :)

we are moving the devel root one dir level up

...

snapshot inverse tranformation

transformation almost finisced, not tested

now inline "file.ma" is allowed.
file.ma must be compiled and all its contents are inlined

Added o.ma (some results about the magnitude of functions *)

initial steps of convertibility

some bits of reduction, reusing psubst

Complete proof of Bertrand for n >= 256.
Removed the baseuri form all files in nat.

Prima versione di bertrand. Tanti cambiamenti qua e la.

baseuris removed from files

fixed dependences

conversion half inplemented

renaming

reordered cases

reorganization of sources

substituion and lifting implemented

renaming

factorized common components of objects

added Local pragma, moved leftno and inductive into obj, added relevance attribute of parameters

added leftno to indtypes, better indentation and comments

nCic almost finished

renaming

regeneration with new results

fixed path for matitadep

fixed make dist

better error message in case inclusion failed

allow to use "../foo/bar.ma" as a path for the include statement

progress.

A formalization of modified realisability with truth as in
``Internalising modified realisability in constructive type theory'',
Erik Palmgren, Logical Methods in Computer Science, Vol 1. (2:2), 2005, pp 1--7.

Bug fixed in generation of elimination principles of inductive types having
at least one constructor of type (A -> i) -> i that was not the last
constructor.

prodT merged with prod
fstT merged with fst
sndT merged with fst

ProdT was a perfect copy of Prod. Removed.
Sum is now in Type.

Results about Chebyshev teta function.

cic defined (half)

Some more theorems.

reindent

oldenv2newenv cache

uri and references(uri)

uri -> reference (2)

uri -> reference

lower bound for neper's constant

sad snapshot

snapshot

snapshot

Improved approximations for A and prim.

Some improvement.

very bad bug found, asert false in cicReduction when a clear is performed

One Obj.magic implemented, trust changed to false.

Transformation back and forth between old and new representation

snapshot

new uri defined

Square root added.

snapshot]

snapshot

added meta for the new kernel

stub functions to make all compile

basic organization of the new kernel

Improved approximations

New approximtions.

...

snapshot with more duality, almost where we left without duality

...

Bertrand's conjecture (weak), some work in progress

snapshot

Matitac now accepts multiple targets :-) (but only in the same root :-(

Hack for code extraction re-linked, but disactivated.

Old tiny freescale experiment get rid of.
New shiny freescale formalization by Cosimo Oliboni <oliboni@cs.unibo.it>,
described in his Laurea Thesis.

Typo fixed.

snopshot before isabellization

snapshot

3.27 ok

yes! the lattice_(#) -> prelattice(<) -> lattice(< -> #) works!

update: upper bound for prim