- ground_2: update ...
- basic_2: first commit for lexs ...

pre commit for lexs ...

general slicing reactivated ...

update in ground_2

- ground_2: support for relocation updated
- basic_2: theory of relocation updated
- MaTeX: (co)inductive types are now processed

- ground_2: relocation with nstream is now based on two basic functions (push and next)
- matex: scope management completed! stylesheet improved (also with colors)

- scope management completed
- improved style sheet and test document

- scope management begins...
- improved style sheet

improved style sheet

renaming ...

some renaming ...

lift functions and identity map

lexicon commands must tbe parsed before grafite commands rather than
after (why?)

documentation update

nstream: composition completed :)

ground_2: web page update

missing notation file

- ng_kernel: catched Invalid_argument "List.nth" in typeof of Rel i (raied when i < 1)
- ground_1: relocation with streams of natural numbers begins

- plain anticipation for CIC proofs terms
- support for (co)fixpoint objects
- Makefile for testing
- minor updates

- Const is now processed properly

more minor bugs fixed in the web site

minor bugs fixed in the web site, and minor updates

site update for helena 0.8.3

- final commit for helena 0.8.3
  minir bugs fixed

minor bug fixes ...

bug fixes ...

byproducts of compilation ignored for svn

- First commit of MaTeX:
  an utility for typesetting the terms produced by matita il LaTeX

- The AST nodes of terms are output as LaTeX macros

- The user configures the desired rendering of terms by
  defining these macros in a LaTeX stylesheet

- Each term inside objects is output in a separate file
  for easy inclusion in the main document

- This softare originates from "coqpp", our appication with which
  Coq terms were typeset in UBLCS 2006-01

as of now,
only Constant objects are accepted and
Const is not processed properly

web site minor update

web site update

update in ground_2

- matita: computed auto traces now include the "width" parameter
          more characters for use with lambdadelta
- ground_2: advances in relocation by trace

theory of relocation updated .....

theory of generic slicing almost completed ....

parked material ...

new results on multiple relocation

theory of multiple relocation completed

minor update

stats updated for ground_2

commit in ground_2

colength and identity relocation

milestone in ground_2

ground_2: added missing file
basic_2: commit of grammar completed

ground_2 milestone: multiple relocation with lists of booleans
basic_2: simplified formalization starts: partial commit of the grammar component

first constructions with classes

optional parameters added to the syntax of definitions,
like the one for Record and Inductive.

limits: we set up a different foundation
lambdadelta: Makefile updated for new version of probe

old files (re)moved

minor site update

refactoring meta files for procedural reconstruction of \lambda\delta version 1

- simplified Makefile.defs using the ?= assignment
- now the variable OCAMLPATH is available and is correctly set

scripts for lambdadelta_1 updated with minor corrections

- the `Implied attribute is now printed
  [also the `Generated attribute is printed. is this ok?]

flavour and source information exported for the objects of lambdadelta version 1

last comment was incomplete by mistake.

- Rationale
  The `Implied attribute will mark the eliminators generated by Coq
  7.3.1 added to the contrib of lambdadelta version 1.
  [the latest version of matita generates different eliminators to
   Prop (with dependences) so we cannot reuse them]
  However, these eliminators, even if provided, must not be taken into
  account when calculating the intrinsinc complexity of the contribution
  on the matita side (by the "probe" tool), because they are not taken into
  account on the Coq side, being `Generated by Coq.

  Note that the intrinsinc complexity we are interested in is the one
  accounting just for the user-defined objects in both contributions.

- probe: updated to handle the `Implied attribute

- .depend: updated

- 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