- New attribute `Implied put beside `Generated and `Provided.
  It denotes an object provided not as defined by the user, but as generated by another ITP
  New optional keyword "implied" recognized in front of:
  theorem, definition, ..., let rec, let corec
  specifies to construct an object with this new attribute.
  [still not admitted in front of inductive, coinductive, record]

typo corrected in bibliography

last commit completed :)

updated bibliography

new version of J3a submitted to JFR

- subtraction (and related notions) removed
- more lemmas

compile-time feature PROFV to profile validation without sort inclusion

grundlagen for coq with timing information

= test2 for byte and opt
- version string management updated

- multi-file exportation for teyjus
- more profiling for helena and coq

more flexibility in the exported data for Teyjus

- conditional compilation continues ...
- current run times for helena and managers in profile.txt

initial support for bytecode compilation

- simpler attribute system
- some renaming

we are optimizing the code by conditional compilation.
three tags introduced so far: EXPAND, PREPROCESS, MANAGER

new semantics of the -g option completed

- bug fix in the static analyzer allows better Pi/forall separation (exportation to grafite)
- new option -y allows to use infinity-abstraction in contexts
- ages removed from global references (the RTM computes them)
- new semantics of the -g option (w.i.p.) for a comparison with Coq

advances on exportation to prolog

command line options rearranged

new options activated
- tracing can be restricted to specific constants with -b and -e
- restricted applications are now used by default for Automath inputs
  use -n to activate extended applications
  (this may lead to longer computations)

new syntax of abstractions propagated to complete_rg

- siimplifified RTM (one register less) now counts x-steps.
  We follow our Prolog implementation more closely.

- Two bugs detected. One solved, the other does not affect the
  Grundlagen.

exportation to \lambda\delta representation in elpi

some changes in lambdadelta butterflies

- revision of ground_2 and basic_2
  lift and drop now accept infinity as first parameter
- Makefile: updated for matitac that now takes directories

performance data for basic_1 on dev.helm

with matita 0.99.2 we can validate lambdadelta_1 (as is) in 4 minutes

legacy_1, ground_1, and basic_1 recommitted without anticipation
this seems to be the fastest solution for now

updated  bibliography for text J1

- new naming sheme for documentation yields more stable names
- update for document J2a

news update and some bugs fixed

basic_1: COMMIT COMPLETED
- component wf3
- additional files
basic_2: some corrections

components: pc1, pc3, ty3, csubt, ex1

components: sc3, csubc

components: nf2, sn3, ex2

components: arity, csuba

component: pr3

components: wcpr0 pr1 pr2

component: pr0

components: A asucc aplus leq llt aprem ex0

- update for helena 0.8.2 and related files
- updated bibliography

additional commit for version 0.8.2
- we add exportation of the kernel entities to coq 8
- coq indeed accepts our translation of the GdA !!
- some improvements in Makefile and README

components: G, next_plus, sty0, sty1

first article on lambdadelta version 3

components: subst1 csubst0 csubst1 fsubst0
we committed almost half of basic_1

components: subst csubv

components: subst0

components: clen lift1 drop1

components: clear getl cimp
if anticipated, getl/drop.ma causes "Out of mamory" in matitac

components cnt drop

some improvements in the anticipator
- we anticipate the terms to be matched
- we do not anticipate inner fixpoints because we turn them into constants when we generate Grafite for the ng_kernel

depend update

components C r flt app lift

- matitac: now directories are allowed as command line arguments
           all .ma files inside these directories are compiled
- basic_1: commit os sections tlt iso

- some improvements in the generation of terms
- basic_1: we commit sections s and tlist

- we generate the terms in anticipated form (the are easier to debug)
- basic_1: commit of section T

porting of basic_1 for the ng_kernel: first step ...

notation ast updated to comply with the toplevel let rec of ng_kernel

refactoring of \lambda\delta version 1 in matita

dependences update

dependences update

informational page on ground_1

basic_1: we separate theorems and lemmas as in basic_2
         the informational page is complete

update in web page for basic_1

- we add an informational page on \lambda\delta version 1 (core)
- web site update

lambdadelta_1: bugfix
Makefile: some improvements

infrastructure to browse lambdadelta_1 remotely

lambdadelta_1 updated with new part names

we restored the scripts of \lambda\delta version 1
(which are now available through \lambda\delta Web site)
by merging and updating all our (not broken) scripts

...

- xhtbl: minor improvement
- web site update
- static xhtml pages from lddl: updated trough ld_web infrastructure

last commit for helena 0.8.2
- a check was missing in the comparator
- new textual syntax for \lambda\delta "Version 4"
  (exp_math files updated accordingly)
- minor bug fixes (BrgOutput now uses the new alpha-conversion)

the corrected "Grundlagen" is online

lddl update with the disambiguated "grundlagen"

- bugfix is refreshed state of AutCrg: now we return a fresh state
- minor changes in the xml format
- some refactoring

removing some old files

finite lambda calculus

A compiling version

- bug fix in the RTM
- we can validate the Grundlagen in lambda-delta version 3

check removed

0.5.9 released

- we add the missing layer constraint on applicability condition
- trace levels refactoring

now type inclusion is correctly managed in the RTM

- we are moving from old (patched) management of sort inclusion
  to new (proper) one via \lambda\delta 3
- some refactoring
- omega.out: committed for reference
- Makefiles: some bugs fixed

- we removed a flag from the kernel status
- some renaming

- helena: the improved attribute system allows to export the sorts of Pi's
  Pi's of sort Prop are rendered as Forall's in the generated Matita script
- we updated the dtd accordingly

fixing

fixing

fixing

dependences update

level disambiguation cmpleted! the Grafite file is succesfully generated.
Matite cannot compiled it yet since it seems to freeze on notion 2760.
We divided the Grafite file in 7 parts for convenience.

- bug fix in the static disambiguation of unified binders
  allows to disambiguate the whole grundlagen
- 20 incompatibilities are detected (AutQE vs PTS)
- matita validates notion 115
- some refactoring

- the disambiguation of unified binders continues
- exportation to grafite is set up
- grundlagen_2: we disambiguate up to notion 6377, matita validates up
to notion 114

- ld.dtd updated
- basic2a.pdf updated
- documentation.html fixed

- static disambiguation of Automath unified binders
  by position heuristics + degree heuristics fixed
  [ grundlagen_2: now 1217 binders out of 47115 remain ambiguous ]
- brgReduction: we did not check the sort-inclusion flag
- new constraints system continues ...

- new attributes system
- new constraints system (starts)
- static disambiguation of Automath unified binders
  by degree heuristics (C.E. Brown)
  [ grundlagen_2: just 1960 binders out of 47115 remain ambiguous ]
- Makefile: XNLDIR is now relative

new intermediate language complete_rg,
more similar to what lambdadelta version 4 should be

new message reporting system improves performance significatively

- commit completed :)
typechecking is approx. fast as before,
validation is slightly faster than typechecking.
for now the new RTM is slightly slower than the old one
- we commit three versions of the grundlagen:
0 (original)
1 (no eta-conversion)
2 (no eta-conversion, no @-typing)

the commit contnues by updating the RTM and modifying the typechecker accordingly