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

quinck and untested implementation of positivity conditions check

...

added depndency of new kernel to metadata to allow to use the DB to calculate the minimum set of graphs to load

FIXED bug, added assertion in case a universe inside a term T living at URI u
was marked with URI v <> u. Unshare.fresh_types should be called!

added a function to linearize a given graph, imperative interface since
is is used only in the new kernel.

added function to fresh types

call Unshare.fresh_types

load the graph of objects that depend on the ones requested,
rank universes and use them in the transformation to obtain terms
with TypeK and not always Type0

use universe rank instead of Type0

Type related failures fixed

better pp of objects

Extracted code. The main executable is medium_tests that runs the emulator on
a few assembly programs with inputs of different sizes:
  * string reverse
  * counting sort
  * perfect numbers

removed useless file

fixed modules order

more fix removed from types

more fix removed from types in proofs

when we build the elimination principle we fresh universes to not
generate tems with different

added a parameter to unshare universes

Conversion of 2 lambdas was not requiring equality on universes of the source type, while the conversion of products was requiring so.
Moreover Coq seems to force that constraint too.

context of types built in the reverse order

added a simplify to prevent the generation of an ugly fix

implemented inductive and less parentheses

The cache of objects is now used also for cofixpoints.

New: cache of translated fixpoints (to avoid the generative fix restriction and
to avoid pollution of the environment). Many more Matita objects now pass.

TODO: the caching machinery should be debugged and better understood (what about
metasenv and subst?)

does_not_occur exported to be used in oCic2NCic

Bug fixed: references to CoFix are CoFix, not Fix.

print unnamed variables as __n

switch off profilers

pp with parenthesis only when necessary and with some more boxes

...

Fixed serious bug that occurred only in the following situation:

\lambda x.
Fix f {
\lambda y: P x.
Fix g {

The two fixes must be translated as

Fix f { \lambda x. \lambda y: P x. ...}
Fix g { \lambda x. \lambda f. \lambda y: P x. ... }

In the first case, the x that occurs in the type of y must be a Rel 1.
In the second case, the x that occurs in the type of y must be a Rel 2.
The previous code translated both of them to Rel 1.

better pp in Appl

better pp

pretty printer on steroids

Added some "\n" here and there to the pretty-printing of Match.

Grave bug fixed: Ce that point to definitions were handled as those that point
to declarations. So Fix-constants were too much abstracted, too much applied,
etc.

added profiling on/off

invalidate fixed

allow to switch profiling on and off on the fly

removed two useless calls to the environment, one still to be optimized out

...

Variables are no longer experted (cooking is now implemented).
Better reporting with indentation.

Swapped arguments in error message.

Variables having a body can occur in cooked terms and must be delta-expanded
during translation to the new CIC format.

Fix over the previous one: Var-LetIn abstractions should be ignored and not
transformed into applications at all.

Error message improved.

Cooking w.r.t. variables with bodies is now implemented as delta-expansion.

Fix name capture in cofix.

To test the translation.

Name capture fixed.

Improved error messages in place of "sort elimination not allowed".

Seed reset before each convert_obj.

Use seed to avoid further name clashes.

...

Incredible, but true! Our name mangling clashed with one identifier in the
library of Coq, generating two functions that mutually called each other,
making the type-checker diverge!!!!

Cooked objects are no longer well typed in the uncooked old environment.
Thus we need to fix_outtype before cooking.