export group_by_tac

drg->brg translation contibued (still bugged though)

qed => nqed.

Now the time required to eval a command is printed.

added code to print the tree

CSC proof made by paramod

more functions

Alias required now ??

new instantiate, only known bug is w.r.t. in/out scope and file matita/contribs/ng_assembly/compiler/environment.ma

the trie indexes terms up to 10 nested applications and skips applications with more then 50 arguments

more auto

Non general recursion implemented via recursion over unary (?) inductive
generated formal topologies.

first bits for the zipper

...

...

more printings

auto is smarter :-)

nauto:
- fixed indexing (now always dome in the same way)
- depth=x means: tray at depth=2 ... try at depth=x
- run auto on set of goals that are linked by occurring in each others types,
  simply distribute if there is no dependency

...

fixed pictures

preserve sharing if map_term_fold_a

add XXX where I found a catch all statement

new sharing-preserving map with accumulator

apply the subst to the metasenv and to p

- Bug fixed: some assert failure were just failures (when processing terms
  that do not satisfy the IRS condition).
- New test ng_bove.ma added to test the Bove-Capretta method (in CProp)

...

Smarter implementation of instantiate to avoid re-checking twice the same term.

...

batch pdf generation

...

some more work

...

...

debug idem for auto added

new lambda instros and better logging

better indexing for auto

some work for auto

some work for auto

removed optimization potentially unsound

...

Profiling code integrated.

 freescale porting, work in progress

Debugging improved.

Benchmarking integrated in folding/unfolding.

 freescale porting, work in progress

cantor...

...

hints were not used by reduction machines on heads

...

ncheck is not erased

...

...

...

...

minor fix

tons of typo fixed

Error message fixed (dereferencing must be done eagerly, not when the error is
actually printed!)

Serious bug fixed: fix_sorts used to allow inference of Type[0]:Type[0]!

CProp uri fixed

...

...

...

...

...

...

Experimental scripts for nth-order rewriting principles.

relocate is hopefully fixed once and for-all!

better screenshot

 freescale porting, work in progress

relocate fixed

better ppcontext

better ppcontext

debug + relocate uses Prop instead of (Prop Prop)... we should think a better solution

one mode debug item

...

no mode middle age debug menu

more comments

...

...

1) Bug fixed: the case Meta(i) vs Meta(i) was handled in a particular way,
   but the case Meta(i) vs (Appl (Meta(j),...)) that reduces to Meta(i) was
   not. As a result, a tempeted self assegniment yielded strange errors.
   Fixed by more aggressively unwinding the subst during fo_unif.
2) Major re-organization of the code to gain some speed in Oliboni's stuff.
   The idea is that of introducing a new internal exception KeepReducing
   used to signal that, after a fo_unif, it still makes sense to fall back
   to machines. Only if it does not it makes sense to distinguish between
   Failures and Uncertain and the latter test can now be implemented more
   lazily w.r.t. the old version that used to call metas_of_term on the
   unwinded machines (that are potentially HUGE).
   With this modification, all Oliboni's tests terminate, even if they are
   still very slow compared to the height=0 strategy. Moreover, the tests
   show that unification on closed terms can still be 4x slower than conversion,
   which is partially unexpected.

Bug fixed: in case of (t ...) where t has flexible type, a failure obtained
without extending ... (since this could cause divergence) should be considered
an uncertain (since extension may be necessary).

Typo fixed.

added last 10 months work...

...

...

new standard library inside path

Closed metas must have closed (expected) types.

Improved debugging code.

...

...

...

no need to compile/install the standard library. if included it
will be compiled on the fly in user space

can live without library db

auto with intro

A new switch to activate/deactive nCicReduction pretty printing.

Printing extremely large terms no longer raises Failure.

drgAut: we fixed the order of multi application arguments
drgBrg: we started the translation from drg to brg

removed misleading context

new discrimination tree instantiation with
inverse De Brujin indexes.

avoid warning