update in grond_2 and basic_2 ...

advances on cofrees allows to prove one direction of
non-recursive characterization of llpx_sn (finally!)

update in ground_2 and basic_2 ...

advances on ldrop ....

advances on cofrees

reordering abstract computation properties and saturation conditions

one file was missing ...

- advances in the theory of cofrees
- some notational changes
- some refactoring in etc

- we introduce recursive free variables of a term in a context ...
- some symbols added

update in basic_2 ...

- name changes in the rediction rules
- theory of extended substitution is active again, we hope to use it
to obtain a non-recurisive alternative definition of llpx_sn

update in basic_2 ...

- the relation for pointwise extensions now takes a binder as argument
- explicit alternative definition of lprs and lpxs removed
- changes in the notation for subclosures and refinements

anniversary milestone in basic_2 !!

3rd anniversary milestone
- recursion removed from alernative definition of lpx_sn
- some corrections and updates

- lazy extended reduction parked
- fpns finally removed
- "big tree" computation based again on "full" extended reduction
  but improved with lazy equivalence for local environments
- llor parked for now (something to fix there)

we restored the strong normalization of extended computation for local
environments with some important updates from the "lazy version"

commit completed: one file was missing :(

- some work on extensions:
  the alternative definition of lpx_sn and llpx_sn is useless since it is recursive
  llor seems to contain a bug in the referred components
- some work pointwise extended reduction:
  we restore the "full" version and use it for the normaliztion of extended reduction
  we still use "lazy" version for the "big-tree" theorem

some advances on pointwise union for local environments ...

some resuls on pointwise extensions (all of them are now in the
"relocation" component

commit completed:
- pointwise ordinary reduction:
  we park the "lazy" version and we restore the "full" version
  annotating the source with our understandings
- pointwise extended reduction:
  we use the "lazy" version for now
  a better understanding of the relationship between the "full" version
  and the "lazy" version (lpx_sn_llpx_sn) allows to link the two

commit of the "computation" component with lazy pointwise extensions
one conjecture is still open :(

update of the partial commit:
we move lleq to the "substitution" component

- partial commit: just the components below "computation"
  the development of lazy pointwise extensions continues ...
- we parked not-lazy pointwise extensions in etc

continuing on lazy pointwise extensions ...

we begin to develop lazy pointwisee extensions ...

update in ground_2 and basic_2 ...

reaxiomatized lleq fixes a bug in it and allows to park substitution in etc

some additions ...

we define the lazy poinwise extension of a relation, that should
allow to derive lleq with corrected lleq_lref, and a new defininition
for lpx (and derivatives), which now contains a bug too :( being not lazy
- we revise the definition of lazy equivakence since lleq_lref contains a bug

some corrections ...

Code changed a bit to make it work as before with OCaml 4.0.
Without this patch, the refresh of the textual widget (e.g. the update
of the locked part) is not immediately done.

This is roughly the visual behaviour the user expects. On the other hand,
we also expect the threads that execute and that responsible for the UI
to work in parallel, which is not the case. The code I just touched stops
the worker thread for, on average, 0.1s per tactic, which is really a lot.
Switching to a multiprocess implementation (in place of a multithread) does
not seem easy. Bad OCaml, bad.

Do not assert false for a print not implemented yet.

Hocus-pocus code to use the old (and deprecated) implementation of
Hashtbl.hash because the new one changes the behaviour of automation,
breaking the library.

Minor changes to make the script more robust to strategy changes.

some external links updated

a suggestion was added to avoid 1 pseudo reduction at the cost of 40 proper
reductions :(

Inclusions improved to allow compilation from the toplevel.

Bug fixed: the tactic to analyze the term and understand whose inductive
type it belongs to did not put the sort in whd before concluding that
it was not a sort.

OCaml 4.0 detects a not handled case.
I hope the assertion will never be reached, but I ignore why.
I think this is really a bug and code must be written there.

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