impredicative Set is considered as Prop in the new check implemented by CSC

New check implemented: the sort of each constructor should be constrained by
the sort of its inductive type.

Note: I just realized that nobody implements the check that the left
abstractions of each constructors/inductive type must be exactly the same.
To be implemented.

Missing check implemented: the sort of each constructors should be constrained
by the sort of its inductive type.

The file bug_universi.ma shows a strage case where the ranked universe
graph does not contain any universe for one object that does contain a
user-provided universe. In turns, this make check.ml fail (since no constraint
is defined between Type0, which occurs in the object, and Type1).

Missing whd.

Bug fixed: since circular <= graphs are allowed, added an avoid list to
avoid looping.
Even more code semplification.
Little optimization: adding x <= x does nothing

Bug fixed: only Type < Type1 was declared.

Bug fixed and further code semplification in management of universes.

The code for universes was not correct in many borderline cases.
The new code should be correct. For sure, it is much simpler, shorter,
characterized by better invariants and its interface has less functions.

ranking reports the lest of univs

added new implementation of universes

added name_of_uri

meta VS meta in alpha_eq honors substitution

used ind/coind information in references

types where compared without lookig at test_eq_only

Timings

(Approximated) inference of relevance implemented: an argument X of t is irrelevant
if it has sort Prop and the sort of t is not Prop.

First implementation of irrelevance in conversion.

New function get_relevance and new (not exported) function get_checked_decl.

New function list_forall_default3. 3 euros to the first one that reuses this function
(not artificially)

Bug fixed in computation of heights: a constant must have height greater than its constant__s

Implementation of calculation of heights.

Typo fixed.

Major code semplification and bugs removed (thanks to a better invariant):
small_delta_step always put the terms in WHNF, even if it can do that with delta > 0.
Terms in WHNF, delta=0 that are not head-alpha convertible and tail-machine convertible
are not convertible.

Removed two args from psubst.

height of constants properly handled

list_iter2_default_value moved to HExtlib. 1 euro to the first one that will
re-use it (not artificially)

eat_lambdas and eat_or_subst_lambdas taken out of the big recursion.
In principle, we could move them to nCicUtils. Maybe this should be done.

debruijn simplified. It could go in nCicUtils, but why should we do that?

Bug fixed: types were check for conversion in the wrong context.

We forgot an important check: the declared and expected type in definitions in
the context must be checked for convertibility.

partial implementation of reduction up to a given height

fixed error message

New checks for well-formedness of metasenvs and substs.

nuri_of_ouri, ouri_of_nuri, reference_of_ouri, ouri_of_reference moved
to NCic2OCic or to OCic2NCic.\fThe kernel is now clean of conversion functions.

Nicer graph.

map_hash moved to HExtlib

New function map_hash.

Generation of dot file.

New licence used uniformly everywhere.

we added a link to lambda-delta home page in the hope that this page gets eventually indexed by google :)

One more bug fixed: we tried to perform List.nth on negative indexes.

More exceptions captured.

Bug fixed in pretty-printing of free Rels.

Never commit before trying to compile... stupid typo fixed.

Used old kernel exception in place of brand new one.

- is_closed removed from the kernel (it used to make a loose test, replaced
  with a tighter one)
- does_not_occur no longer calls lift (performance improvement)
- does_not_occur: bug fixed in management of Metas

Library factorized out.

wrong test equality only fixed

Type of conjecture and subst_entry made uniform.

convertibility was taking a metasenv but not using it

Added boolean "is_inductive" to NReference.Ind

trust is always false by default

trust implemented, but in the nCicTypeChecker!

New implementation of CicEnvironment:
 a) I have splitted out nCicLibrary from nCicEnvironment
 b) Recursion changed: the nCicTypechecker now registers itself to the
    nCicEnvironment. Then it is the nCicEnvironment.get_obj that retrieves
    an object from the library before calling the registered typecheck_obj
 c) The logger is now called every time NCicTypechecker.get_obj is invoked,
    both by the nCicEnvironment and by another module

TODO: implement trustness

height is stored in the reference, no need to fetch the object from the environment

fixed english

valid xml

...

...

released 0.5.0

...

...

some files orphaned

...

a missing prime

Bug fixed: the domain of a LetRec was only made by the last function in the
mutual block.

Update after some more bug fixing.

Partially reverted bad merge by Enrico that re-introduced an un-conditioned
whd in guarded_by_destructors.

More bugs fixed.

get_check_fix and cofix unified, bug regarding debruijnation of constructors types fixed everywhere.
the constructor typs are debruinated wrt some inductive type uri an not wrt
their own, thus a wrong context was created. guarded by constructors ported from the old kernel.

get_checked_indtys can take a constructor reference

added mk_cofix

let corec

CoFix cache implemented

fix_left_in_constr still broken, ask enrico

guarded_by_constructors implemented, some cleanup here and there.
fix_lefts_in_constr fixed: the inductive type list was returned with
constructors instantiated and debruijned, but with types whose arity was
instantiated with lefts too. This is wrong since we want to use these types to
build a context, that is closed, and will be put at the end of the actual
context since debruijn will make uris point to those terms

removed dead code

...

Bug fixed in handling of explicit named substitutions: it could happen that
explicit named substitution are merged not in the expected order. This happens
comparing the case of an instantiation inside and outside a (nested) section.
Thus I have added back the re-ordering of the explicit named substitution in
CicSubstitution.subst_vars and in CicReduction.unwind_aux. Moreover, I have
added to CicTypechecker.type_of_aux' the check that verifies if an explicit
named substitution is ordered.

Broken XML files either fixed or removed.

Some destruct tactics got broken after last update. Small axiomatization
still included.

More precise classification of failures.

List of all URIS comprising:
 - coq objects
 - matita standard library
 - all matita tests and matita contribs that compile today

More options can now be set at the beginning of the file.

Last (???) bug about variables with bodies fixed: we do no longer create
applications with less than 2 args.

Another case where the presence of variables with bodies resulted in the
creation of an application without arguments.

tagging 0.5.0-rc1

Bug fixed: application without arguments generated in case of an ens made only
of variables with bodies.

New bug found.

Things are getting better.

Implementation of guarded_by_destructor is now complete w.r.t. the old kernel:
 a) bug fixed in eat_lambdas_etc: we cannot apply the term to the residual
    arguments since these are not left arguments
 b) when the recursive argument of the nested "let rec" is safe, the formal
    argument can also be considered safe.

TODO:
This implementation of condition b) could be improved by re-writing eat_lambdas
in such a way that it uses a shift_k function to add the context item to the
"context".

Reducing an open term should not be an error (or should it be???) and it
should not raise Failure (that's for sure!).

stupid error fixed

fixed_args fixed to accept passing a partially applied fix to a fix that
passes itself partially applied to anothere fix

added check on all bodies, only the one we actually encountered is applied to all arguments, other boedies are applied only up to j

added fake uri when the univ is anon

fixed wrong Rel, still to do: Fix(i,j) applied to dangerous rel, check all bodies in parallel, not just the i-th

universes are written with the URI inside objects, this allows
universes to be actually shared between objects and no duplication is necessary.
in this way the typechecker is more strict and unification can be an ungly beast implicitly
adding an = constranint between two universes. speedup granted!

xml strict!