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

new macro screenshot

we improved the stylesheets and we generated the static HTML pages

...

xml: bug fix
Makefile: now we should be able to generate the static HTML pages

xml: first ld to xml stylesheets
Makefile: we now generate index.txt
dual_rg: automath encoding fixed

...

new tactics by CSC

new implementation of delift_type_wrt_term, that call delift directly

huge commit regarding universes:
- only Type[foo] can be declare with a strict (<) constraint among other
  Type[bar]
- CProp[foo] is automatically available for Type[foo]
- The CProp hierarchy can be collapsed (hopefully in a consistent way)
  to both Prop OR Type:
  - You cannot eliminate CProp to build a Type like for Prop/Type
  - You cannot eliminate Prop to build a CProp, like for Prop/Type
- Peculiarity: CProp[i] has type Type[i+1], since CProp[i+1] is only >=
  of CProp[i] to allow collapsing them (while < whould be violated).

New function to delift a type w.r.t. a term list, to potentially build a
dependent type, used in lambda_intro and Letin expected type propagation.

...

we start version 0.8.1 by replacing the abstract layer AST with a fragment of dual lambda-delta. To this aim we begin the dual_rg kernel

one more exception printed

more work for igft

more notation for topologies, and some prentheses that can be used in notation

some more work...

New interesting coercion.

The left parameters coming from the constructor types have been refined in a
longer context. Thus we need to unify them in the longer context (that does not
hurt those coming from the inductive types).

improved check in delift for flexible lc entries.
added a function to easily delift a term w.r.t.
other terms, thanks to delift, used to propagate the expected type
of a letin.

some renaming. final commit for version 0.8.0

fixed coercion mechanism w.r.t. undo/require

Slightly simplied status code.

Simplest typing for status records.

New tactics ncut and nlapply.

a nice bug in meta handling is not visible... brr...

some more letters

...

constructor accepts the arguments of the constructor...

new tactic constructor: @[n]

...

new syntax

let rec/corec and co/inductive are not printed!

new macro ncheck. fixed term2pres for Inductive and LetIn=Cast

ok, but slow on includes

nice hints

maledetto il \sub di CSC

it starts to work

nice notation for hints!