Final implementation of proof irrelevant conversion, which hadn't
been committed (!)

better debuggin output

error...

...

another divergence case patched

to avoid a case of divergence small_delta_step checks if terms are flexible and
gives 0 as delta

...

we can test the unification algorithm!

...

commented out unfinished code

...

- setters for data structures now support "commuting conversion"-like
  operations w.r.t. getters
- several axioms have now been proved
- new file env_to_flatenv1 showing an alternative representation of the
  environment

...

unification completed

...

librarian.ml: now the read_only .moo's are managed "correctly" (i.e. better than before)

...

quick fix to make read-only baseuri non compiled but considered successful

...

updated changelog

added UBUNTU/

more push/pop to avoid confusion with imperative data structures employed by
notation.  the patch is not well tested, but already improves the situation
make the library compile again. I commit it so that on monday we will have
again the livecd and the .dsb package that are required by the sysadmins to
install matita on the cs cluster

Procedural: we removed some commented code
matita/Makefile: tests re-enabled
character: scheduled for daily testing

include statement better implemented:
- push/pop operation for both Lexicon and Grafite stuff, instead of reset
- this (if properly working) opens the doors to a completely functional
  matita status

fixed some notational collisions

auto was compiraing lazy proof terms with = ... fixed

iremoved call to auto

commented out a line that was making the file fail

lazy proof term to increase sharing and decrease memory consumption.
I hope nobody was comparing grafite-statuses with ocaml polymorphic =

some work

...

...

...

beta expand

...

...

...

...

...

...

...

added skip function

...

...

...

new iterator

new small devel

fixed auto invocation

we commented some of the debug pps rather than removing them :)

snapshot

snapshot, cicMsubst compiles

more abstract discrimination tree

added list_seq

snapshot

better abstraction to allow 1 discrimination tree implementation for both the
new and the old CIC

new discrimination tree

Revised discrimination tree implementation:

- code size reduced, looking for unifiables or generalizations is
  almost the same and do not internally work with the query term,
  but its path representation that is now decorated with arieties to
  recover the tree structure when needed (jump to the sibling...)

- works with partial instantiation (no more global ariety list, but
  local to application heads). Stupid example:

  query: fold plus [] 0 = 0
  ==?==
  tree: fold ? [] 0 = 0

  since the 2nd arg is ? we skip the query subterm rooted in plus,
  but if plus is considered of ariety 2, we fail unifiing the following
  terms (we skip [] and 0 reaching the second 0 that is unified with
  [] and fails).

- term -> path string function fixed to clen up the input term, no more
  "FIXME: the trie received invalid term". Here there is room for improvements
  especially on beta redexes and terms beginning with an abstraction, but we
  need the substitutions operation, we should move the file elsewhere

- Big change:
  - if the query term is a meta, then the whole content of the tree is returned
  - in paramodulation this is dangerous, thus we added a small check in
    the paramodulation code (eq_indexing) instead of making the discrimination
    tree behave in a nasty way
  - the new implementation returns the same set of candidates on all test
    TPTP/Veloci and library/ (except for the aforementioned corner case).

more comments and compare function for URI exported

removed debug pps

new reorganization

fixed

A temporary patch to demodulation theorem.

removed debug pps

applyTransformation: improved error detection
library: new depend and svn:ignore

librarian: improved error detection, bug fix in time comparison functions: now the object files are considered in the correct compilation order even if they mtime is the same :)
Procedural: improved error detection

ppterm_in_named_context removed in favour of the high-level pretty printer.
Much nicer error messages :-)

Major reordering of theorems in the appropriate files.

In case of coercion to Prod, the error message shown is that _after_ the
coercion. In case of multiple coercions, only one error is shown.

fixed script

Precedence level of \downarrow changed to match that of the binary one.

snapshot

...

formal_map now defined

Definition of formal_topologies.

...

...

...

...

new directory for the newGeneration refiner

BTop is a category.

old bug in mtime computation fixed

...

1) as usual, I took the reverse notation for composition.
   "fixed" according to the internatinal tradition
2) partial proof that basic_topologies form a category

helm mailing list moved to cs.unibo.it

we skip discharging on matita opbjects (they don't have exp. variables)

cicDischarge, Procedural: we improved debugging and added some time stamps
librarian.ml: new algorithm for sorting sources according to compilation order

reverted auto experiment

AGAIN A TEST

COMMIT TO JUST RUN A BENCH, SHOULD BE REVERTED ASAP (auto run after every tactic)

Reordering of lemmas in proper places.

Concrete spaces do form a category, after all :-)

some work to make tries "printable", fixed comparison of constants in
paramodulation, added (but commented) a call to auto after every tactic
invocation to test it on the whole library.

Getting closer thanks to more technical arrangements.

...

...

Concrete spaces now defined.

Case c1 t1 vs c2 t2 where c1 and c2 are not splitted and t1 and t2
are rigid was not handled correctly. Fixed.

cicDischarge: we still have some problems here. Some fixes
cicTypeChecker: added some debug prints (commented for now)
applyTransformation.ml: improved error detection

we always save the discharged object for future reference

we have to remove the Num directory :)