milestone update in basic_2!

- we commit just the components before "reducibility"
- reaxiomatized substitution and reduction now commute with respect to
subclosure
- delift and thin removed for now

uncommited file found :)

commit by user andrea

commit by user andrea

commit by user andrea

commit by user andrea

Fixes a bug that caused an assertion failure when no notation was defined.

Patch by Paolo Tranquilli. It fixes the following problem: when a new
tab was openened, the interface got confused about which script was focused.
It did not save the previous focused script if it was at end of file and
it saved it instead when switching from the new tab. Other bugs could be related
to that.

commit by user andrea

update in basic_2 and apps_2

- new component for restricted computation (delta, zeta and tau only)
- subclosure preseves native validity asexpected
- some renaming

update in basic_2

- parallel substitution reaxiomatized
- supclosure reaxiomatixed (now commutes with parallel substitution)
- some refactoring

- probe: recursive removal of empty directories
- matitadep: improved parsing of input

missing or rootless dependences now don't break the compilation process

some additions

update in basic_2

a file was added by mistake

- more understanding of the "big tree" reduction step

sfr renamed as lbotr and its symbol changed according to lsubr

notational change for lsubr:
now looks like the other refinements for local environments

lsubs renamed as lsubr

notational change for snv and lsubsv: inverted "!" used for now

milestone in basic_2!

- lambdadelta: last recursive part of preservation finally proved!
  some notational changes
- BTM: one file was missing
- probe: now sources and objects not having a .ma file are deleted

this is the real update :)

update in basic_2

- main proof case closed in the 4th component of preservation
- bug fix in Makefile: now both xoa and probe receive both
configuration files
- useless notion lsubss removed (to be replaced by lsubse)

- lambdadelta: third recursive part of preservation finally proved!
  Makefile: xoa.conf passed to probe for future use
- xoa, probe: now can *really* take several configuration files

more results on lenv refinement for stratified native validity

bugfix in web tables

some bugs fixed

- xslt and Makefile improved, web pages regenerated

Chpater 4 and 5

- improved Makefile esp. with the "trim" function
- some files trimmed

chapters 2 e 3

we removed a useless assertion that was forcing matita to edit just matita files
matita's editor is good on its own and has interesting facilities including predefined virtuals
in lambdadelta we use matita to edit the .tbl files containing notation from the .ma's
and we use matita as well to edit predefined_virtuals.ml
we still wonder how we could do this up to now despite the assertion!

- update in basic_2
- contrib specific web pages moved out
- improved Makefiles

basic_2_src.tbl was not updated :(

- lenv refinement for stratified native validity redefined
- contrib specufic web pages moved here

second recursive part of preservation finally proved!

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.