Proof-irrelevance check for all applications (first version)

incomplete irrelevance test commented out

Some proofs on enumerator and denominator.

More work on rational numbers with unique representations.

some work on uniformity

end of section 2.2

proof refactored

xxx

more work on supremum

CProp hierarchy is there!

Implications:
  - more universes, XML file format changed, please rebuild your stuff
  - CProp conclusions are eliminated with _rect and not _rec
  - CProp and Types are interleaved, but still comparable, this may (or not)
    what you expect: Type_i < CProp_i < Type_i+1 < CProp_i+1

Caveats:
  - are_convertible sort CProp may turn to be wrong, since Type_i is convertible    (<=) to CProp_i+0.5 and there is no way to set test_equality_only, an
    additional parameter may be useful
  - CProp goals will be tackled by auto even if they could be cumulated into
    Type that is not (by default) take into consideration

irrelevance check half implemented but already impossible to
complete

...

garbage removed

more work on dama

prod moved under lambda-prolog unification case

added CProp

thanks to the fact that we convert well typed term and that
we convert only types, by inversion we know that types of lambdas
source are convertible if in head position

added a bit more reduction in case Prod v.s. term, was just head_beta_reduce, now is full whd

relevance check partially implemented but bugged since cic:/matita/nat/compare/eqb.con is not ok!

case not unfilding fixed

CProp, since it was defined in CoRN as a Type, is predicative.
However, it is not Type0, but a moving Type as usual, for example

  inductive and (A,B:CProp) : CProp := ...

  inductive exists (A:Type) (P:A->CProp) : CProp :=
   | ext : \forall x:A. \forall p : P x. exists A P.

does not pass since the sort of x is Type not included in CProp. Putting
exists in Type does not work either, if you want to make a conjuction
involving an existential.

solution, to be implemented:

  CProp of CicUniv.universe

where CProp n is meant to be Type (n + 0.5).

0.5.1 released

unused variables removed

ref sync check fixed controlling fix/cofix coherence

...

first page of the new dama proof

...

the type of the match was obtained reducing the outtype
applied to right + matched with whd ~delta:true that
is not what you want. replaced with head_beta_reduce.

...

dama restarted

cleanup

the attempt of completing dama using duality frozen

0.5.1

...

smarter lexer needed by lambda-delta that is splitting "let rec" statements
on multiple lines

...

CoRN moved in contribs

frst step to move away the CoRN stuff

frst step to move away the CoRN stuff

auto calls cleanup\

better description of declarative tactics

new, more rigid syntax, for auto_params affecting the declarative language.

many multi-word constructs (like 'we proved') are now a single token.
all declarative tactics now use auto_params.
syntax of declarative tactics changed.
many camlp5 refactoring to avoid many rule conflics.

Universe.key was not used to index terms, but was used to retrieve them

better presentation of lambda-delta

- some bugs fixed in the domain-based preorders on environments
- some missing lemmas added

added comment for zack

...

auto syntax updated

...

...

order of goals changes, open ones are preferred to closed ones as in the paper

minimal implementation of left parameters display

0.5.1 should be realased soon, the bug that was affecting fixpoints
disambiguation is nasty

Here is where we should add relevance checks.

Bug fixed in computation of leftnos: variables were not considered.

Code simplification.

Added cprop <= type constraint.

We do not need to give cprop a special status yet.

...

CProp dropped in favour of a cprop universe exported from NCicEnvironment,
which is just an URI recognized by the pretty printer.

added leftno to references f inductive types and constructors, more unifor names of modules, NCic -> C and NReference Ref everywhere

added aps generation

Dummy dependent types are no longer cleaned in inductive type arities.

...

renamed add_le_constraint to add_constraint since it adds both le and lt constraints

...

Dummy dependent types are no longer cleaned in inductive type arities.

run fsub during night

Bug fixed: when computing the left arguments, I was not doing the right thing.

New check implemented: references should cache data correctly.

Dummy dependent types are no longer cleaned in inductive type arities.

Dummy dependent types are no longer cleaned in inductive type arities.

Dummy dependent types are no longer cleaned in inductive type arities.

names fixed accoding to the new ones generated after arity of
indtypes is not cleaned for dummy names

Dummy dependent types are no longer cleaned in inductive type arities.

Dummy dependent types are no longer cleaned in inductive type arities.

Dummy dependent types are no longer cleaned in inductive type arities.

revert last commit, context' -> context (added comment)

using the right names in the context to check match patterns(better error report) and use the refined matched term to compute the type

Dummy dependent types are no longer cleaned in inductive type arities.

Dummy dependent types are no longer cleaned in inductive type arities.

Dummy dependent types are no longer cleaned in inductive type arities.

Dummy dependent types are no longer cleaned in inductive type arities.

New missing check implemented: the left parameters of each constructor and
inductive types should be convertible and should have the very same name.

Dummy dependent types are no longer cleaned in inductive type arities.

Dummy dependent types are no longer cleaned in inductive type arities.

Dummy dependent products in inductive types arities are no longer cleaned.

This commit avoids cleaning dummy dependent types in the arities of inductive
types. This is an overkilling solution to the problem of avoiding cleaning
dummy dependent types in the left products in the arities of inductive types.
The left products should be _syntactically_ the same as those of the
constructors. Otherwise, error reporting is incorrect.

Implemented translation of inductive types from the new to the old format.

Serious bug fixed: the max of two universes was computed using the polymorphic
max function of OCaml instead of append!!!

Synch with the paper.

...

Error message improved.

More effective optimization: avoid introducing already implied arcs.

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.