- 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

- cpxs_tsts_vector completed
- refactoring in etc

cpx_tsts completed

- tdeq must imply tsts
- notational change for tsts
- refactoring

update in basic_2

main part of lfpxs_cpxs ...

update in basic_2

cpxs_drops completed

update in basic_2

cpxs_lfpx completed

update in basic_2 and apps_2

- advances on lfxs for lfpxs
- ex_cpr_omega (2-steps loop)

update in basic_2

advances on cpxs and cnx (cnxa removed) ,,,

update in basic_2

- advances on csx
- corrections in the web page

- initial support for sigma-types
- matex.sty: some style improvements
- test.tex: red boxes arround hyperlinks removed

csx on the way ...

update in basic_2

- advances on cnx
- generic reducibility moved to the "static" component

- one annotation added
- web page updated

milestone in basic_2

support for generic reducibility ...

update in basic_2

update in basic_2 ...

- cprs and cnx on the way
- breaks repositioning in notation
- corrections in NF and SN
- refactoring

update in basic_2 ...

- advances in rt_transition
- bugs fixed and refactoring of some parked files

- comparative table of the core objects started ...
- some bugs fixed

update in basic_2 ...

- some commutations between the rt-steps and the s-steps proved
- some bugs fixed

update in basic_2

- updated equivalence on referred entries: it nust be degree-based
- refactoring

- degree-based equivalene for terms
- improved matitadep allows to find more top files in the reference graph
- refactoring and bug fix

update in basic_2 ...

update in basic_2 and ground_2 ...

- improved fqu allows to prove fqu_cpx_trans and its derivatives
- parked frees_fqus_drops that does not hold anymore

update in basic_2 ...

- preservation of arity assignment
- hls orders files by extension and then by name

update in basic_2 ...

- improved lfpr_lfpr
- improved make stats (it was still invoking mac)
- hls.ml to list .ma files highligting the ones updated to basic_2A2

milestone in basic_2!

lfpx_frees and confluence of lfpr!

previous lemma proved ...

improved lsubf allowes to prove lsubf_frees_trans.