better spacing

statistics are used, when possible, to sort
constants

Added statistics printings

Added statistics module

First proof finished (some tactics still not working).

matitaprover is now flexible enough to allow the computation of statistics on
the clauses and then choose an ordering to be used for the proof search

Coercion hiding implemented. Notes:

1) hiding of coercions whose return type is a product is not done correctly,
   since the "sats" information seem to have changed semantics. Enrico, is it
   a bug or just a new semantics?
2) coercion matching has been implemented trivially (O(n)) in NCicCoercion.
   Here I need a special version of a discrimination tree. Enrico, do we have
   one already or is there a way to simulate it?

 freescale translation (work in progress)

Composite coercions are here!

- brgOutput: the nodes count is now implemented
- brgReduction: the type annotation in the beta-reductum is useless
- brgType: a never-occurring condition marked with assert false

initial implementation of coercion composition

more work on coercions composition

 +root +depends

Removed unused parameter of unification procedure (vars)

more profilers

Coercions used here and there.

Bug fixed (missing ctx) + comment added.

...

new ng freescale, no external dependencies

Let's live with new ocaml type system limitations...

initial implementation of `ncoercion name : type := body on name : pat to pat`

claudio, please have a look at this

new nrepeat (and block '('...')' ) tactical

...

New functorialization: paramod is abstracted over a Orderings.Blob, that is like Terms.Blob but adds the compare_terms function.
This allows an easy instantiation of the main loop with differend orderings

Fixed check for condition iv p.33 (Riazzanov)

More updates to Fsub.

profile most operations, do not return a filtered varlist in unif (useless and expensive)

1 process for now

two cases should be assert false at least in TPTP

micro optimizations to unification

Cleaned a bit

...

activate kbo, not lpo

...

Bug fixed (non-captured variable).

eq moved to CProp
In Prop a unification problem was not solved, but I suspect that that was
a bug...

...

repeat_tac

...

few more files, one diverges

directory for porting the assembly to matita-ng

removed useless universes

import of a sample for cosimo

Hmmmm. This way we need "canonical structures" also for local definitions => BAD

...

Metavariable case in does_not_occur (hence weakly/stricly, positive, etc.)
relaxed. Is this always correct??

Missing case for Match implemented.

...

weakly/strictly positive checks relaxed to allow metavariables that are not
substituted

...

Improved error message.

Bug fixed: the debrujinate function (hence the one to compute objects height)
did not take the substitution.

...

Bug fixed: one uri was not refreshed, causing divergence of the kernel!

fixed some typos

Let's play a bit with NG.
This library is NOT meant to be the final one, just a way to experiment with
features.

1) Include files for NG were neither recursively processes nor accumulated.
   They are now recursively processed (is this the best solution???)
2) Bug fixed (an assertion raised in including an included file because of
   a false assertion on references)

Fixed printing of number of problems solved

Tried to implement lpo in a more efficient way

Fixed typo in lpo (from old implementation)

some corrections

more static analysis on the Automath text

Ported old implementation of LPO (for test purposes)

we now do some static analysis on the Automath text to possibly clear some language ambiguities

Implemented LPO

Corrected type for bag

New age selection
New demodulation strategy

better output handling

return type of paramod fixed according to the SZSOntology

...

...

Version number set to 1.0.0-rc1

Fixed type of bag

parallel

Moved ID management inside the bag

attempt of using 2 different orderings

....

Corrected a few typos

...

Enabled age selection (ratio 1/5)

lambda-delta:
- lib/output: infrastructrure for reduction reporting
  we found just one instance of "referene typing" in the "Grundlagen"
  rt.txt reports where it occurs
- lib/time: bugfix
- basic_rg: bugfix (some relocations were missing)
  the "Grundlagen" now typechecks :)

...

do not infer on closed goals

removed a maybe diverging test

...

First attempt for refined goal selection strategy

added (but not active) last chance idea

Implemented orphan murdering technique

new make test target

new kernel basic_rg: implements ufficial lambda-delta with de Bruijn indexes

attempt to run a last chance procedure after the timeout

the timeout is passed to test last chance

this case is not assert false since it can happen if occur_check
makes fail the unification

fixed parsing

convenient problem lists

an easy for loop

deep subsumption activated