Different behaviour of OCaml 4.0.

update in basic_2

some additions for the forthcoming presentation

update in basic_2

- some corrections and additions
- lsubr moved from "relocation" to "static"

Porting of HOTT from Coq to Matita.

* Overture.ma half completed up to truncations.
* PathGroupoids.ma is next and should depend only on
  the part of Overture that has been ported.

relabelled documantation entries

update in web site and basic_2

- we bypassed another false conjecture :) ...
- minor corrections

addition of unused material :)

update in ground_2 and basic_2

a wrong conjecture bypassed!

update in basic_2 and ground_2

- main proposition on lsx finally proved!
- long awaited equivalence for local environments is now set up (coequivalence is in etc in case of need)
- unused results on append parked in etc
- some additions to ynat

- a reinforement in a lemma on ldrop allows to prove a lemma on lsx :)
- some renaming

- improved definition of lsx allows more invariants
- some additions
- we parked some unnecessary planes (cny, cpye)

update in basic_2 and ground_2

some advances on reduction

evaluation for context-sensitive extended substitution (cpye) completed!

we start total substitution ...

some notation renamed and fixed

normal forms for extended substitution

bug fix in the notation of normal forms, now we specify that they are
normal forms for reduction. This will allow to enable normal forms for
substitution ...

Almost there

progress

some corrections ...

working version

nat: we added a non-indexed theorem
lambda: the corrispondence between terms by level and terms by depth
is proved!

more auxiliary machines

- nat: some additions, plus_minus_commutative renamed plus_minus_associative
- lambda: we study terms in which references are by "level" rather
than by "depth" aiming at establishing a bijection between the two
representations, we start the support for distributed notation as in lambdadelta

milestone in basic_2

commit completed: now we support two versions of slicing for local
environments

- commit of the "reduction" component with two additions ...
- formal bug fix in extended substitution under a binder: now we
follow the paradigm used for reduction under a binder

commit of the "unfold" component ...

commit of the "static" component

- commit of the "substitution" component
- some renaming
- we disabled the old notation for ldrop to capture its instances
syntactically

commit of the "relocation" component with the new definition of ldrop,
the other components will be committed shortly ...

we start a criterion on extended computation

some improvements on the relation lsx ...

update in ground_2 and basic_2

new definition of lleq allows to complete the proof of lemma 1000
(lleq_cpx_conf_dx)!

- ynat: some additions
- lleq: we are ready to remove the old definition :)

one file was missing :)

- lleq now uses ynat
- some bugs fixed

- new definition of lazy equivalence for local environments,
  driven by extended multiple substitution for terms
- minor corrections

- extended multiple substitutions now uses bounds in ynat (ie. they
can be infinite) for use in lleq
- ground_2: additions in ynat

more arithmetics for natural numbers with infinity ...

some improvements and new lemmas for
natural numbers with infinity

the theory of extended multiple substitution for therms is complete
a simpler theory is complete as well but parked in etc for now

theory of extended iterated substitution begins ...

theory of cpy is complete!

the theory of cpy continues ...

refinement for extended substitution completed

- lsubr moved down one component
- extended substitution started (for use in lleq)

update in basic_2

eliminators of arited terms based on "big tree" proper computation

update in basic_2 completed

one file was still missing

update in basic_2

commit is now complete :)

- "big tree" theorem is now proved up to some conjectures involving
just computation
- redefined "big tree" proper computation now replaces its restricted
form and is transitive
- improved definition of "big tree" proper reduction involves lazy
extended computation for local enviroments

- first results on strongly normalizing local environments
- some updates

partial commit ...
- fleq removed and replaced by fpns
- improved proper "big tree" reduction
- some missing lemmas

update in basic_2

third commutation property on lazy equivalence for
local environments proved, multistep version

New approach: we use "iterator" steps in place of pointers.

update in basic_2

first and second commutation property on lazy equivalence for
local environments proved (lleq_fqup_trans, lleq_cpxs_trans) multistep
version

1. more bugs fixed
2. correctness proof completed

update in basic_2

- last patrtial commit of the "reduction" and "computation" components
- we generalized a lemma

More progress.

Some progress in the correctness proof and a bug fixed.

initial commit of the "rduction" component

update in ground_2

commit of the "substitution" component and of some auxiliary files ...

- improved arithmetics for natural numbers with infinity
- some properties of equivalence for local environments
- improved lazy equivalence for local environments
- we commit just the "relocation" component

A first example that uses a status monad where the status is a tree.
It should be possible to implement it imperatively and efficiently.

addition for natural numbers with infinity

update in ground_2, web page for ground_2

definition of equivalence for local environments,
based on natural numbers with infinity

web page for ground_2 and bugfixed statistics generation in the Makefile

strict order relation for natural numbers with inifinity

- natural numbers with infinity for lambdadelta

update in ground_2 ...

- xoa: the definitions file now includes the notations file
- probe: improved "list" algorithm, and bugfixed "remove" algorithm
- lib/lambda: updated and bugfixed dependences to cope with new xoa
- lambdadelta/ground_2: decentralized and bugfixed notation, now copes
with new xoa, some refactoring

Final version of the binary machine (all proofs completed).

Closes many daemons.

Full rework of the semantics of the binary machine (now completely working
up to arithmetical proofs)

Almost finished...

Major bugfix/reorganization/improvement of the partial proofs: full semantics
of the binary machine should now be easy.

update in basic_2

second and third commutation property on lazy equivalence for
local environments proved (lleq_cpx_trans, lleq_lpx_trans)

update in basic_2 (bugfix)
probe was not run so statistic data were outdated

update in basic_2

- lambdadelta: first commutation property on lazy equivalence for
local environments proved (lleq_fqu_trans)
- matitadep: now three input syntaxes from grep are understood

lazy equivalence for local environments is now defined
its reflexivity reveals a bug in ldrop :(

Splitted star

update in basic_2

- lambdadelta: tentative definition of lazy equivalence for closures +
Makefile update/bugfix to support matitadep update
- matitadep: bug fix in redundancy check + new option shows leaf
nodes