- star.ma: constructor inj of star conflicts with previous constructor
inj of TC. constructor inj of star renamed to sstep and constructor
injl of starl renamed to sstepl
- lambda_delta: bug fix in reduction rule tpr_zeta which now has the
structure of like tpr_delta. More lemas towards subject reduction of
native typing

adv_to_mark_l

closing a few axioms

additions to basic_2

- relation between native type and atomic arity proced
- higher order native typing defined
- some minor results towards subject reduction for native typing

middot notation

adding match_machines and removing trans_to_tuples

several changes

Reindented

New nohyps option for /demod/

New flags for demod:
  1) by ... now can be used to explicitly give the set of equations to use
  2) nohyps can now be used to avoid using the hypotheses

move_char.ma
-This line, and those below, will be ignored--

A    turing/move_char.ma

merging of char_move_c and char_move_l

A recompiling version

Dropping a coercion and some hints due to conflicts with CerCo

Modifications and refactoring

Msg reporting via HLogger in the error window made asynchronous => speedup.

Patch to avoid generating _inv_ind_recTX for X the largest universe.
Rational: for some unknown reason, that takes ages to fail.

Sys.Break no longer catched

New debugging switch in the interface.

More conjectures proved.

new version of move_char_l suign swap

swap machine; move_char revisited

restructuring

Restructuring

Some results on relations. Moved things around.

Completed all proofs in if_machine

an addition to basic_2

- lambda_delta: subject reduction for nativa type assignment begins ...
                dependecnes between source files improved
- matitadep: little application for optimizing dependences between .ma files
             (used by lambda_delta Makefile)

semantics of the if-machine.
Moved some lemmas to their proper places.

notation

comments

additions to basic_2

- predefined_virtuals: an addition
- lambda_delta: lenv ref for native type assignment completed
                levn ref for substitution correctly oriented

Finalized copy sub-machine of the universal turing machine. Some new results
on lists.

Ci siamo quasi

update in basic_2

- predefined_virtuals: some additions
- lambda_delta: first results on lenv. ref. for native typing
                some notational changes

Thanks to Guarrigue, code for Serializer functor simplified using
private types. The type system of OCaml is more and more misterious...

Progress.

update in basic_2

- nDestructTac: Sys.break handled in two places
- lambda_delta: a major property of native type assignment
                some properties of context sensitive equivalence
some notational changes
some annotations

Progress.

some progress

Progress.

Progress.

The universal machine!!!

trans_step.ma

porting move_tape.ma

porting move_char_l.ma

porting of move_char_c

more typos

typos

graph of a function

FinOpt

mem, split

Progress.

tentative specification of Conway's construction for surreal numbers
matita.opt game.ma crashes after 4 lines of code :((

update in basic_2

- substitution lemma for native type assignmenr proved!
- notation change in the support for abstract c.r.'s
- some minor additions

Progress

Porting to the new defintion of finset

New definition of finset.

a bit faster

Progress

Progress

Progress

Progress

Progress

Progress

Progress

Progress.

Added move_tape.ma

Progress

New version of init copy

Progress

Progress

init_copy init_match

Progress in semantics of the copy machine.

depenences fixup

init_match

Progress

Progress

Added step machine for universal machine.

...

...

Efficient hashing used.

hash function exported

The lpo cache is now implemented as an hastbl for more performance
improvement. Probably it would be better with an ad-hoc hash-function.

move tape right

filtering on a list without repetitions

Added null character.

Added cache to lpo implementation.
The current cache is based on imperative lists.
Can it be improved with smarter data structures (e.g. HashTables?)

Orientation of equalities is now displayed.

Orientation of equalities is now displayed.

Removed duplicated notation and interaction with the user.

update in basic_2

- a caracterization of the top elements of the local evironment
refinement for substitution
- notation update for subsstitution and unfold
- added notation for True and False

Compare was not compatible with eq!
The first used alpha_eq, the second did not.
Now both do.

New, faster implementation of lpo checked against old one.
Old code removed.