Bad variable name fixed.

Bug fixed: projection redexes obtained reducing other projection redexes were
not reduced.

New version using Streicher's K axiom. Should be faster and also work with
indexed inductive types.

Added Streicher's K axiom.

Fixed a bug with indexed inductive types which sometimes prevented the
inversion principles from being defined.

 freescale porting

lists

Booleans

boolean arithmetics

 freescale porting

minus

On the last goal at maxdepth we stop at the first solution.

 freescale porting

 freescale porting

 freescale porting

minus in nat.ma

Nuova gestione della width.

 freescale porting

 freescale porting

le_arith

Unfolded exact letins during proof reconstruction.

Added a parameter no_implicit (default true) to choose between raising
assert false or returning the identity.

 freescale porting

le_arith

 freescale porting

 freescale porting

 freescale porting

 freescale porting

 freescale porting

Esempio

 freescale porting, work in progress

We can always use the "covered by emptyset" relation...
Closer and closer to Bove-Capretta, but more and more far away from IGFT...

More //.

More // everywhere.

// used everywhere!

// in place of nauto everywhere

// is now more powerful

// is now more powerful

New paramod tac.

Invocation of paramod

paramod_tac exported

Number notation for NG

Number notation for NG

Number notation for NG.

Keeping Implicit for refinement (instead of transforming them to Metas:
context bug).

Updating.

A slightly more complicated example.

Finished!

We are still equivalent (even if the definition of ncover is obfuscated).

Urrah!

Extending to the nAx set.

Skipfact function (a partial general recursive function) defined by recursion
over the cover relation of an IGFT.

Fixed a bug in the discrimination principle: the refiner was not able to
synthesize the return type of the inner match correctly.

Finished

1. New paramodulation function
2. goal narrowing works both on the current goal both before and after
demodulation

saturate cust be called with delta=0

Added is_equation

Debugging info

Improved

Partial porting to new syntax.

Source language path must be appended, not replaced.

Categorical stuff postponed.

The body of constants is a reference, not the actual body!

removed debugging info

rebuilding the library

rebuilding the library

rebuilding the library

applyS

refresh uri
applyS

Support for the new auto tactics //

Support for the new // tactics.

new reloc_subst (to avoid cyclic substitutions).
Changed default sig.

....

...

...

Simplified.

Note: it breaks the file later (maybe a coercion conflict, I suppose).

Coercions via unification hints?

- we now add the kernel options in the preamble of the URI hierarchy
- we now quote the identifiers by default to make them NMTOKENS but we added a command line option to disable this quoting (it can be time consuming)

1) stuff moved from categories.ma to setoids*.ma
2) we are now ready to define the category of o-algebras

...

Almost done (up to definition of category).

Porting of Sambin's stuff started.
Everything is now automatically enriched using hints.
It seems to work quite smoothly.

Porting of Sambin's stuff started.

Removed line is back again.

...

Refining with no expected type + unification seems to be faster.

Trying to be faster

Trying to be faster.

Final subst returned by superposition and passed around.

using = instead of alpha conversions. context metasenv and subst are not
needed any more

eq_coerc for smart application.

the sort hierarchy parameter enter the kernel status

Minor bag fixed, relative to failures.

A compiling version?

Added a "sort_metasenv" function.