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!

allow @{ ... } as the identifier of the letin

to me, the problem:
  ? t ==?== ?->?
where the first ? has an empty local context
is always Uncertain... to be fully understood
why unification gives Failure. It may be correct if
t has type (Rel k). I wrap it in the refiner.

some interfaces improved

more stuff fixed

the refiner was not checking that the resulting type
of an application was the expected one in case
the application is ((lambda...) ?...) when ?...
resolves to the empty ? vector.

some fixes here and there

depends

some more work for ng-coercions

some renaming and some interfaces improved

snapshot for CSC

snapshot for CSC

basic_rg: more improvements to the error reporting interface

basic_rg: we improved the error reporting interface

the TypeError exception is back in place inside the Type modules
basic_rg: some typing-related code is back in place inside the Type module
log: some improvements in the interface

Reduction speedup (a.k.a. better sharing):

The ~delta argument was accidentally saved in the closure of aux that was
passed to all functions defined by the reduction strategy. So, most of the
terms where shared by the KAM environment in whd normal form with delta=max_int
(that means, not delta/iota-reduced at all, just beta-normal).
Thus many heavy computations where not shared, completely loosing the point
of having a KM.

The solution was to fix the API so that delta is not hidden anymore, then
really sharing computations with delta=0 (the most common case, I think).

The bad behaviour is still present for other values of delta, and an imperative
cache may be emplyed.

Reduction speedup (a.k.a. better sharing):

The ~delta argument was accidentally saved in the closure of aux that was
passed to all functions defined by the reduction strategy. So, most of the
terms where shared by the KAM environment in whd normal form with delta=max_int
(that means, not delta/iota-reduced at all, just beta-normal).
Thus many heavy computations where not shared, completely loosing the point
of having a KM.

The solution was to fix the API so that delta is not hidden anymore, then
really sharing computations with delta=0 (the most common case, I think).
The bad behaviour is still present for other values of delta, and an imperative cache may be emplyed.

 freescale porting, work in progress

 freescale porting, work in progress

 freescale porting, work in progress

 freescale porting, work in progress

 freescale porting, work in progress

fix to speedup reduction making intermediate conversion problems smaller

fixed eliminator name

some work

CIC has no eta-reduction/expansion

do not fail if the inductive type is mutual, just do not generate the eliminator

decent error on interpretation declaration

fix double app in Ast

better print of ILLEGAL applications

lint target improved

basic_rg: bugfix in AST to allow attributes in global entries
xml: the exported XML data now comply a DTD
icons: crux icon for the browser's address line
Makefile: "lint" entry added for XML validation

catch wrapped exception

alias bug revealed

...

initial and incomplete port of the old demo about inductively generated formal
topologies. we try to make slightly different choices...

exponentiation should output with \sup not with ^, that is meant to be an
input only notation.

added "already defined"

ncoindutive now generates a co-inductive type, not an inductive one

Meta case not handled, the iterator was complaining.

Nicer proof "finished" (up to arithmetical facts).

- alpha convertibility test disabled for now (it needs better implementation)
- some icons related to lambda-delta are now available

Towards a simplified proof.

...

Injectivity proved! What a mess...