partial commit: "conversion" and "equivalence" components ...

partial commit: "computation" component ...

partial commit: "reduction" component

partial commit: "unfold" component

partial commit: "static" component ....

partial commit: just the components before "static" ...

- the milestone was not reported on the web page!
- we say on the web pages how nodes are counted

milesone in basic_2!

- probe: critical bug fixed (all objects were deleted due to wrong test)
- lambdadelta: lenv refinement for atomic arity assignment updated,
               some renaming and notational change
reaxiomatization of beta-reduction complete! (milestone)

lambdadelta
- we changed the beta-reductum to make reduction a special case of
  extended reduction, the lenv refinement for native validity was
  updated accordingly
- we parked restricted reduction, substitution and lenv refinement for
  static type assignment
- active notations are now one per file and are included by nead: this
  avoids time-wasting recompilations when notations are added, removed,
  or changed
- Makefile: some speed up, uses new version of mac, handles auxiliary
  xoa files that can be included by need to avoid time-wasting
  recompilations when xoa objects are added
mac
- now outputs the pages count
probe
- minor bug fix: exceptions during file removal where not cought

milestone in basic_2

- new extendedd beta-reductum involving native type annotation
- extended strong normalization for simply typed terms (milestone)
- some renaming

partial commit of the components before "conversion"
- some work on extended reduction and computation
- some renaming

update in basic_2

- bug fix il ldrop (interesting), fsup, fsups
- now fsupq is the reflexive closure of fsup, as expected
- some renaming

- partial commit :(
  some work on supclosure and extended reduction ...

update in basic_2

more results on extended reduction

some work on extended reduction ...

update in basic_2

redundant dependence removed

- a comment removed

- induction on supclosure replaces induction on weight for closures everywhere
- bug fix in csn_alt

update in basic_2 and apps_2

- basic_2: induction for preservation results now uses supclosure
relation rather than weight on closures
- app_2: "functional" component updated
- we park delifting substitution for now

iteration.ma

bounded quantifiers and pidgeon_hole

gap.ma

Nuovi files

commit by user andrea

commit by user andrea

commit by user andrea

Error to debug

Improved version

more functions

partial update in basic_2

- some renaming
- finally we issue the "dynamic" component

partial commit of the "dynamic" component

partial update in basic_2 ...

- partial commit: we issue the "conversion" and "equivalence" components
- we park conversion and equivalence on local environments for the moment

partial commit in basic_2

partial commit: finaly we issue the "computation" component ...

- partial commit: refactoring in the components before "computation"

partial update in basic_2

- partial commit (just the components before computation)
- we park head normal forms for the moment
- some refactoring

reverse complexity

Bumped to 0.99.2.

Missing include.

chapter9

tutorial

Old version dropped.

New notation for congruence

This line, and those below, will be ignored--

M    chebyshev/chebyshev_psi.ma
D    chebyshev/chebyshev_B.ma

commit by user ricciott

A few integrations (closed an axiom in finset).

commit by user andrea

commit by user andrea

commit by user andrea

commit by user andrea

commit by user andrea

An attempt at ostensiby named syntax.

update in basic_2

one file was missing

- we commit the "reduction" component
- we park the focalized reduction for the moment
- some refactoring

update in basic_2

refactoring should be completed now

refactoring completed :)

- we are committing just the components before "reducibility"
- first definition of "unfold"
- notation bugfix
- some refactoring

commit by user lroversi

commit by user andrea

Fixes a bug which caused Meta_not_found exceptions to be raised after qed-ing a
lemma with unskipped goals closed by side-effect.

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)