Injectivity proved! What a mess...

...

- Bug fixed in definition of big_op.
- ltb now goes to booleans
- the meaning of big_x n is to sum from 0 to (pred n);
  in particular big_x O is the neutral element.
  Thus the isomorphism is broken.

...

- sort inclusion must be restricted to term backbone in order to avoid
validity of non-normalizing terms (see the omega.aut example)
- command-line options -a and -p rearranged

One half done.

...

...

...

...

- alpha conversion check added to the brg kernel (succeeds 1/4 of the times)

- performance data added for reference
- interface of the Hierarchy module improved
- library for managining abstract layer representation files added
- toplevel improved: the analysis of the automath source is now optional

- proper KAM with closures implemented for the brg kernel

- kernel parameters indication added to exported objects (xml)
- some refactoring

...

...

Since the introduction of saturation, an assert false is now possible
(i.e. locked meta vs non flexible term since some saturations have not been
fully performed yet)

 freescale porting, work in progress

- xml exportation activated for the brg kernel
- improved Makefiles

(nat,plus) is an abelian, unital magma

Some quick patch to fix elimination that used to look for
nat_rect_max{CProp0,Type0}

fix_sorts (cfr. previous commit) used to break too many things.
This commit is a more conservative extension...

Assert false do not allow to debug...

Let's refresh the universe to avoid assert failure.
However, the effect of this is still unclear to me.

 freescale porting, work in progress

A very little bit of arithmetic.

 freescale porting, work in progress

 freescale porting, work in progress

 freescale porting, work in progress

 freescale porting, work in progress

basic_rg: improved interface, unwind removed from applicability check
basic_ag: improved interface
common: kernel code sharing started

 freescale porting, work in progress

The first omomorphism theorem for whole sets (i.e. setoids + morphisms, not
sets + morphisms).

Hmmm: I don't see much gain here.

Metas must be handled when using iterators.

Setoid rewriting as unification hinting. Does not work recursively yet.
(Why??)

 freescale porting, work in progress

 freescale porting, work in progress

 freescale porting, work in progress

 freescale porting, work in progress

 freescale porting, work in progress

 freescale porting, work in progress

 freescale porting, work in progress

 freescale porting, work in progress

More Gonthierism. Are they the right solution?

...

Hmmm, quite broken now.

 freescale porting, work in progress

 freescle porting, work in progress

 freescale porting, work in progress

 freescale porting, work in progress

Smaller formulae.

 freescale porting, work in progress

 freescale porting, work in progress

Setoids, setoids1, sets, and the like. The mess begins.

Note: the (partially) interesting part of the development is that canonical
structures (provided by unification hints) allow to perform setoid rewriting
by hieroglyphs without having to use "rich operators". On the other hand, after
the application what you get is always an enriched structure and thus either
it is normalized away or the theory becomes a mix of rich/unrich. The latter
phenomena happens anyway because, in algebraic structures, you need to put
things in rich structures to have all the properties you need.

algebra/magmas does not work because refinement of projection is too weak

Bad patch reverted (in error message).

Bug fixed: one case of too many arguments was not detected and used to diverge.

Serious bug fixed: uris were not refreshed when loading coercions.

Record projections are now defined as fixpoints in order to block
delta-expansion when the argument is not a constructor.

\ldots are now used in nelim and ncases

Pp fixed in order to obtain read-back.

1) \ldots here and there
   Where they are not used, it means they do not work!
2) napply/etc. now add \ldots at the end by default

More napply \ldots => napply

napply now automatically inserts \ldots at the end

More \ldots.

\ldots used here and there. Cool!

First implementation of \ldots.

Note: the implementation is now inefficient since implicits are generated and
mapped to metavariables again and again and again. It would be better to handle
\ldots as a coercion from \forall x:A.B(x) to B(?).

...

Don't reinvent the wheel.

Added benchmarks

 freescale porting, work in progress

New demodulation (innermost, optimized to avoid reducing already normalized
subterms).

Changed the ordering of rels, and the introduction of hypothesis to get
a version closer to the standalone prover.

Lazy strings
-This line, and those below, will be ignored--

    paramod.ml

Added the benchmark with the new demodulation function.

"..." -> "\ldots" for implicit vectors

1) Some more work for vector implicits.
2) Vector implicits can be used only in argument position.

Introduction of vectors of implicit (only for NG).
Proposed concrete syntax: "..."

New reference benchmark with CPU Time

Removed meaningless time information

Removed internal default timeout
Added TreeLimitedRun (CASC) script to run_on_a_list

Stupid bug fixed: the test to detect Uncertain cases was simply reverted.

Removed old logs

Useless "let module" removed.

Since I guess the divergence bug is fixed, I activate the test again.

Serious bug fixed: because of lazy evaluation of !require1, the function could
diverge.

setoids.ma split into setoids.ma + setoids1.ma

topology/igt.ma (???) |-> sets/setoids.ma

...

Moved benchmarks to new folder

It works better now.

...

No more hand-made coercions.

Debugging code removed.

Record fields declared as coercions as now really declared as coercions.

Beta-expansion was avoided as soon as one argument was flexible.
This lead to a different behaviour in the following two unification problems:

   (\lambda_.?) ? =?= T         vs               ? ? =?= T
     or, equivalently
        ?[?] =?= T

The fix is very easy: we always perform beta-expansion and delifting will
take care of ignoring the flexible "arguments", both during beta-expansion
and during the unification that follows.

...

Function to map NCic.term to CicNotationPt.term finished.
Note: it is almost identical to ncic_of_ast0, but it uses a different data
type for contexts that allow to perform "substitution" in a single operation.
Moreover, the terms that are substituted are CicNotationPt.terms and not
NCic.terms. The two codes really ought to be unified.

Bug (found during code review) fixed (but not tested and bug never re-produced):
wrong context passed around.

...