update in basic_2

improved "big treee" computation allows to close a case in the
preservation proof

Bug fixed: let-rec defined propositions are no longer extracted.
They used to be extracted, but in the interface the type abstraction was
wrong.

update in basic_2

- lambdadelta: we removed focalized reduction from snv preservation
- matitadep: bug fix in loop detection

update in basic_2

- lambdadelta: first recursive part of preservation finally proved!
- lambda: bugfix in include paths, now they are relative to the root
- matita.lang: keyword "fact" added (used in lambdadelta)

chapter2 revisited

Quick patch: the maxmeta is now pushed/popped when compiling an external file.
This is implemented imperatively for now. It should go into a status.

Quick patch: the maxmeta is now pushed/popped when compiling an external file.
This is implemented imperatively for now. It should go into a status.

Bug fixed: composite coercions were not extracted.

Bug fixed that reveals a new one: in case of inductive types defined via
let rec, it used to happen that a "type 'a foo" in the .mli was implemented
by a "type 'a foo" in the .ml. Now the opposite happens in other situations.

Ferruccio's removal of objects commented out because it breaks compilation of
the standard library!

Chapter 1 revisited

when we serialize the contents of a .ma, we remove the old objects
before adding the new ones

- xhtbl: now double quotes can appear in string literals
         built-in help completed

- nUri : added Sets of uris for use in "probe"
- probe: now we can exclude the objects of dismissed sources
  (those in .matita/ but not in the development as .ma)
- lambdadelta: Makefile now uses the new feature of "probe"

update in basic_2

- "big tree" order implemented
- some annotations

trace added in a failing invocation of auto :-(

update in basic_2

substitution lemma for stratified native validity!

update in basic_2 summary

we rephrased sstas in terms of star

update in basic_2

we reformulate the extended computation to simplify the proof of its
normalization property

statistics update in basic_2

- first piece of the mutual induction for preservation finally closed!
- a conjecture closed

an update in basic_2

more service lemmas in nat and lambdadelta

one table was nissing ...

update in basic_2

even more service lemmas ...

A few integrations

restructuring

restructuring

update in basic_2

- lambdadelta: more service lemmas ...
- matitadep: bug fix due to new invocation from Makefile

some missing files ...

Bug fixed: .ml/.mli files were opened/closed even when ocaml extraction was
not active.

Bug fixed: "open X" were not printed in .mli because streams are destructive.

Flushing needed before closing the channel.

Improved exception handling.

Bug fixed in pretty printing of mutual inductive types.

Bug fixed: the indty can be typed with a Prod, not only with a Sort.

New option -extract_ocaml to extract to ocaml files.

Pretty printing of ocaml files slightly improved.

Last known bug unrelated to names fixed: a fixpoint that creates a type used
to be extracted in the wrong way.

state mte2 renamed to mte_acc

...

converting certain basic machines to composed machines

defs.ma was never really used

Makefile to extract to ocaml code.

Oops, part of last commit (ocaml extraction implementation)

Ooops, this completes the previous commit (ocaml extraction implementation).

Implementation of Ocaml extraction (largely ported from Coq).
Note: yet to be thoroughly debugged.

In order to use, recompile everything with "OCAML_EXTRACTION=1 ocamlc".

Identity change, improves readability.

- Now the nodes count does not include the generated objects

lambda finaly moved in lib

match now only uses the new move operation

- ng_refiner:
  now the expected type is `XTNone (was None), `XTSome (was Some, also
  was `Term), `XTSort (any sort, was `Sort), `XTInd (any (co)inductive type).
  `XTProd (was `Prod) is used in "try_coercions"
- we replaced some instances of None with `XTSort or `XTInd through the code.
  lib, lambda, and lambdadelta compile,
  in case of errors like "the term ... is not a sort" or
  "the term ... is not a (co)inductive type", revert to `XTNone in the
  corresponding check.
- Now generated objects have the `Generated attribute properly set
- lambda: many "?" removed because of the improvement in the refiner
          other instances of "?" removed for other reasons

Speed-up in match.ma.

Proved old axiom.

Yippeee! Completes proof of soundness of the universal machine
(multi-tape formalization).

unistep!!!

update in basic_2

- notation change for weight functions (following lambda)
  that used to clash with the lref construction
- some parentheses added arround application arguments

funzioni ausiliarie

cfg_in_table_to_tuple

sem_copy_strict

many axioms and daemons removed

quasi finito

well-foundedness done

sem_exec_move completed

almost there

A lot of changes

Splitted unistep_aux
Added another semantics for cfg_to_obj

started unistep

progress in termination

- paths and left residuals: forth case of the equivalence proved!
  The proof is now complete!!

finished semantics for termination of match machine

progress

progress

- paths and left residuals: third case of the equivalence proved!

progress

termination!

Universal machine

Removed all axioms in unistep_aux

removed daemons

universal

tape_move_obj completed (modulo daemons)

cfg_to_obj completed (modulo daemons)

progress

semantics of unistep

- paths and left residuals: second case of the equivalence proved!
- some additions to lstar and Allr

progress in cfg_to_obj

copy char form obj to cfg at the end

high level semantics

high level semantics