beginning of minimalist foundation from a student of Milly

Horrible workaround

Compiled with recent OCaml, Matita now fails removing
a notation when it starts. The patch avoids the assert
false. I have not investigated what's going on.

.depend{.opt} files changed

Patch to make it compile with recent OCaml

added .gitignore

OCaml special files ignored

patch to make it compile with recent OCaml versions

strange bug-fix to allow compilation on recent ocaml+camlp5o

Stupid fix to avoid new camlp5 bug with int64 literals

Patch to make it work with new versions of lablgtk2

- work in progress proceeds for the new definition of voids ...
- arith.ma: some additions and reordering

an addition for \lambda\delta

work in progress on a new definition of voids ...

the previous commit was incomplete :(

work in progress with fle ...

work in progress ...

- free variables innclusion (fle) encapsulates some complexity
  in the proof of a generalization of frees_lfxs_conf
- a refactoring solves a bug in dependences

update in basic_2

- equivalence between lfpxs and lpxs + lfeq proved
- more descriptions in basic_2_src.tbl

- lpx and lpxs restored to prove equivalene between lfpxs and lpxs + lfeq
- Makefile: number of objects and intrinsic loss factor added in summary for web page
- basic_2_src.tbl: more descriptions

update in basic_2 and in the corresponding web page

- equivalene of tc_lfxs and lex + lfeq proved
- bug fixed in fqu_lref_S

- ground_2: rtmap: disjointness relation
-           lib: some additions
- basic_2: first version of tc_lfxs_inv_lex_lfeq
           some improvements
           new explanatory column in basic_2_src.tbl

- dependences on ceq and ceq_ext fixed
- lfeq (was lleq) reintroduced
- some renaming

former commit completed: one file was missing :(

- ext2_tc added
- lexs_tc reconstructed
- support for lex (was lpx_sn) reintroduced
- fixed a bug about ceq

notational change in basic_2

- notation change for tdeq and related notions
- extra spaces removed in notation files
- bug fixed in replace.sh: the case of a wrong sed should be handeled correctly

update in basic_2

- lsubsx (replacement of lcosx) completed
- minor updates

- some proposition name clashes removed
- advances on lfsx_csx

advances on lfsx_csx ...

update in basic_2

lfsx_drops completed

update in basic_2 ...

- exclusion binder in local environments allows to complete lfsx_lfsx !
- advances on csx ...

update in basic_2

- exclusion binder in local environments
  the update is now complete, after bugs fixed in lfdeq.ma
- minor corrections

updated colors for summary tables in the web site

- cpxs completed
- changed colors in sunnary tables for web site

update in basic_2

- exclusion binder in local environments
  portions updated of: cpxs, lfpxs

update in basic_2 and apps_2

- exclusion binder in local environments
  component "rt_transition" completed by updating: fpb, fpbq
- one example file now works

update in basic_2

- exclusion binder in local  environments
  updated: cpm, cpr, lfpr, cpc
- some refactoeing and minor corrections

- update in basic_2
- "versions" table fixed in the web site

one file missing in previous commit :(

- exclusion binder in local environments:
  cpg, cpx, lfpx updated
- notation for lazyeq: fixes and additions

- one conjecture closed on lsubf
- some renaming in rtmap_sor

update in basic_2

- exclusion binder in local environments
  updating of component rt_transition started
  cpg completed

post milestone in basic_2

- exclusion binder in local environments
  component i_static updated
  (this is part of last milestone)

- milestone in basic_2
- update in ground_2

- exclusion binder added in local environments
  working components: syntax, relocation, s_transition, s_computation, static
- improved lsubf of which we hope to prove transitivity
- improvements in rtmap

update in basic_2

update in basic_2 due to previous update in grond_2

- web site update
- update in ground_2

- more results on relocation
- refactoring

notation bug due to previous refactoring

xoa notation refactoring and minor additions

one file was missing :(

more results on binders ...

extension of a relation to binders

component utf8_macros fully renamed

component syntax_extensions was not declared

more notation for s-steps

notation for clear

notational change for lexs

one file was missing :(

- more background for the exclusion binder
- some corrections

refactoring completed

refactoring ...

some improvements before setting up the exclusion binder

- notation for the exclusion binder in local envirinments
- advances on lfsx

- advances on lfpxs ...
- some instances of Conf3 discovered
- some refactoring

milestone in basic_2

- strong normalization for rt-comutation
- advances on lfpxs ...

lfsx_lfpxs completed!

- lfpxs based on tc_lfxs
- documentation improved with the attribute "uses"
- cpre and cpxe parked for now

advances on lfsx ...

update in basic_2 ...

- first prroperties on lfsx proved
- component "conversion" completed
- some typos fixed

advances non lfsx ...

- lfsx started ...
- advances to complete csx_aaa

update in basic_2

- strongly normalizing terms form a candidate of reducibility
- one application of auto is unnecessarily slow,
  a longly awaited improvement of auto is needed to solve the issue

we always update OCAMLPATH rather than leaving it unchanged if defined

removed unused timeout flag

removing extra spaces

- csx_cnx_vector.ma completed
- refactoring

csx_lfpx.ma completed!

- advances towards strong normalization
- refactoring of properties with relocation

we finally understood what tsts is, :)
so we renamed it as theq

advances on csx towards strong normalization of rt-computation ,,,

nilestone in basic_2 !

component rt_transition completed!

update in basic_2

- more commutations with superclosure: fpb_lfdeq
- lfpx_lfdeq_conf, whose proof is much simplified w.r.t. basic_2A1

- fpbq
- advances on lfdeq towards lfdeq_lfpx_conf