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!

many pending modifications were there, now the website at least validates

guarded_by_destructors on steroids

  when Fix/i args and some args are not guarded
  1) fixed params in interval 0..i are checked for bewing just passed around
  2) the fix is unfolded, debruijned, fixed arguments substituted,
     not fixed arguments pushed and checked for guardednes
  3) a new function with relative fixed arguments (not to be checked again)
     is added to k
  4) the resulting term is applied to the remaining arguments

  testcase: cic:/Suresnes/MiniC/MiniC/State/sizeOfType.con

added list_mapi

Tests status update.

speedup in fixing the graph closures

Avoid (whd ~delta:true) during guarded_by_destructors as much as possible.
Note: it is better to check again if this commit is fully correct (i.e.
w.r.t. the catch-all case in the main "match ... with" of the aux function).

In guarded by destructors, avoid computing the (whd ~delta:true) unless the
check fails. This is a major speed up, for instance for
cic:/Coq/ZArith/Zsqrt/sqrtrempos.con

Update...

No more bugs on guarded_by_constructors in the old kernel.

When going under a binder, a term must be converted twice, as explained in the
previous commit. The problem is that in this way the complexity of the
translation becomes O(2^n) when n is the maximum depth of binders. However,
this computation is completely unuseful if no (co)fix is found in the term.
This commits adds as much lazyness as possible to fix the issue.

Proof of adequacy.

guarded_by_constructor completely rewritten, fixed missing lift when generating the context of an inductive type in guarded_by_destructors.

added coinductive example

Working and broken URIs.

ported the instantiate-left-params-to-calculate-rec-args patch from the old to the new kernel,
to test the patch properly some steps of substitution inside a possibly blocked fix are performed,
this should be in general avoided without good checks (still to understand)

Avoid other comparisons on universes using =.

Avoid code duplication.

Do NOT dare using Pervasives.compare on data structures containing URIs!
Use UriManager.compare to get a 2x speed-up in type-checking setoids.

oblivion ugraph everywhere outside the kernel

slow_implementation and some dead code removed

more strict check by CSC, I miss it

fix cache comparison relaxed to URI and not REFERENCE

added a call to ppcontext in the case of appl, to ease the localization of the error

added ppcontext

Types for LetIns computed during parsing for Coq objects may contain universes
that must be made fresh.

defn2.ma is to be used with part1a_inversion3
the induction/inversion lemma in part1a_inversion3 is more regular w.r.t.
 the meta-theory
automation pushed to its limits in part1a_inversion3.ma

fix universe handling, newly encountered objects are typed in an empty ugraph
that after the cleanup phase is committed into the cic_environement and merged
with the current one.

minor reformatting of sources and some more for_all

Alternative prove using just one induction/inversion principle.

better error message

...

impredicative set work around

impredicative set work around

associativity of -> fixed

ancient graph regarding universes and trust=false, universes calculated for internal objects
were used for the toplevel object (that should be sound) but cleaned using the univ list of
the internal object

extlib list_uniq instead of local copy

ranking function fixed: when graphs are collapsed one step links are not updated (nor serialized to disk)
thus you can not rely on them, just use the closures!

added flag to change Set into Type on the fly, that helps on some coq objects using impredicative set

oblivion_ugraph => empty_ugraph

Added to flags to activate/disactivate pretty-printing and exception catching.

Uris must be stripped of their xpointers.

Dead code removed.

Inversion lemma for Forall.

workaround for Pi associativity

workaround for some Set/Type problems

cicEnvironment refactoring with sound view of Coq`s univ-less terms

assertion was wrong, an object can contain a named univers if its uri is the one of the object itself

graph generation phase fixed

Appl case in is_really_smaller fixed as in the old kernel

example:
  inductive I : Type :=
  | k : \forall A. (A -> I)-> I

  match t with
  | k _ f => f w (* is smaller than t even if applied! *)

added a missing whd

new calculation of recursive parameters in guarded by destructors:

  inductive I : Type :=
  | K : list (pair Type I) -> I

  let rec f t on t : I -> bool :=
  match t with
  | k ((nat, x)::_) -> f x
  | k _ -> true

is now accepted. the arg of k used to be recursive but not the head of the list
(only its tail) since constructors types were not specialized on actual left
arguments (and the information that the type of the head contains I was lost).

Two similar cases packed together

some fixes for guardness conditions

is_really_smaller in sync with old kernel, impossible cases removed

check_is_really_smaller simplified to consider that it is called only on terms
(immediately put in normal form) that inhabit an inductive type. Moreover,
some duplicated code has been removed.

1. bug fixed: the context must be type-checked before using it in type_of_aux'.
   Otherwise get_cooked_obj raises Not_found in Deannotate
2. big improvement in guarded_by_destructors: when a fix applied to a safe
   argument is found in the body of another fix, the body of the inner fix
   is check adding the recusrive formal parameter as an additional safe
   argument.

get_checked_fix -> get_checked_fixes

added comment

added sample of guarded by in which coq is stronger

positivity check fixed, a MutInd not applied (but with an exp-named-subst)
was considere non strictly positive always

do not use an implicit but a sort as a neutral term for positivity check

objects are typechecked to ensure there is a graph before doing all the stuff... read: much more memory is required

leftno should be increased of the expnamedsubst, but counting only the uris of vars without a body

better error message

same_obj made more precise, fixed the order of the context for fixpoints body,
cache of fix extended to the mutual case (properly)

ficed fixpoint cache usage for mutual fix

fixed positivity conditions

added mk_fix i j r that given an r of a fix generated another fix on i and j

positivity condition was relying on the name declared in abstractions, and
was checking for a dependent product calling does not occurr with a wrong
index

added little optimization to not add twice the same arc