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!)

...

better static html pages, now they are generted in the install location

- delift_type_wrt_term fixed in many ways
  - as a side effect let in expty propagation works
  - as a side effect lambda_intros now works
- is_flexible (delift) improved in case: (? args) ---subst---> (\lambda .?) args

fixed the type of tactic_term, attributes were useless

instantiate merges tags

added sortification for (? args), untested code

sortification simplified

fixed off-by-one

With this hint, it diverges.

rewritten instantiate code

New datatype for metasenv/subst: full fledged attributes in place of optional
strings.

Added initial support for inversion principles in Matita NG.
Added a case_tac tactical, performing goal selection matching metavariables by
means of their associated tag.
Added tagged implicits, which are refined as tagged metavariables.

Better (but still broken) fix for the case ?sort vs ?term.
To implement the right thing, we need to be able to mark metas as sort without
using the fact that their type is an Implicit.

The term contains dummy.conv that was searched over the net.

1) improved (???) debugging, with
  1.1 more messages (good)
  1.2 messages for exceptions (very good)
  1.3 vim folding/unfolding (good or very bad?)
2) bug partially fixed (to be improved/totally fixed):
   when we unify a ?n:? vs a term t, we need to check
   that t is a sort! (or a flexible term??? what to do in that case?)
   otherwise we can get ?n := O and ?1:?2:?n=0 which is a not
   well typed metasenv. Hence boom later.

...

Re-indentiation

ugly coerc db print

The unification does not longer use the refiner (urrah!)

...

...

more virtuals

...

It does not work recursively...

...

non ho resistito!

- fixed bug in coercion application, input/output swapped in unification
- experimental automatic reduction of projections in apply-subst-metasenv

2 lift related bugs fixed!

better debug pp

Experiment...

Experiment...

Type printed as such, CProp printed as such

fixpoint have attributes for pragma (i.e. they can be marked as projections)

...

...

...

...

...

multi screenshot

ncheck works in the current ctx

...

....

...

...

...

...

more on screenshot