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

...

removed printing

we enabled the new style xml exportation, in particular for dual_rg

Performance improvement by preserving more sharing. Visible in Oliboni's
development. But still slower then old matita (but pheraps on different data...)

terms indexed in the automation cache are saturated

short names

auto works on the regular tactics status

the wrap function takes a string argument so that we know
which wrapper function failed

unfocus can be performed also if all goals are closed

Debugging code commented out.

fixed Ref generation

- oCic2NCic and nCic2OCic moved to ng_library
- spurious dependencies of ng_library on modules that need to convert
  old tables added; to be removed in the future

drgOutput: bug fix
we maked the non-tail recursive functions in: lib, common, automath, dual_rg

removed useless stuff

some fixes

drg: we added the "positive projection" in environments
top: we enabled the automath/drg transformation

fixed constructor on non inductive type

Syntax highlighting for 'ninverter' keyword

Inverters/Inversion:
- fixed a bug with left parameters and inversion principles
- hooked automatic definition of inversion principles to the declaration of
  inductive types

unification pps can be activated by the menu debug

...

nAuto W.I.P.

Improved error message.

new toplevel: tentative implementation with more CPS

- common/entity: new format for kernel entities
- common/library: new CPS infrastructure for XML exportation
- toplevel/meta: now uses common/entity
- dual_rg/drg: some fixes
- dual_rg/drgOutput: XML exportation started (alpha-conversion is missing)

...

...

...

auto and auto_paramod are in nAuto

new file for auto

downcast removed

added auto_cache in the dupable status after an
re-factoring and re-typing of the whole serialization
code.

new ng_library module

uffa

...

Does not compile! Wrong unification hint?

...

...

...

...

hints fixed

fixed bug in coercion application, input/output swapped in unification

if the query has a completely flexible side, the empty result set is given

hints input is cleared from projection redexes

projections redex (proj (mk_foo ...)) where mk_foo
is explicit (not the result of a reduction) are
always fired.

on the contrary, when the delta avoids the reduction
of a projetion (since the arg reduces to mk_foo but
for a smaller delta) we store in stack not the reduct
but its original version (before reducing it to delta=0).

This seems nice anyway, and a FIXME is left in the code

Updated command ninverter. Syntax:

ninverter <id> for <indty> [<selection>] [: <target_sort>]

It is the same as the previous inverter except that:

- <selection> is now optional (when it is omitted, every index is selected)
- the user is allowed to specify a <target_sort> (when it is omitted, ninverter
  defaults to Prop, as it was the case for inverter)

better nlet rec boxing

Wrong context (again!)

...