loc * lazy string -> (loc * string) lazy

disambiguation now returns and takes in input the substitution

...

...

...

...

...

dama almost ok

...

...

reverted

dama into the library

x2sx declared as coercion and used when possible

renaming

...

0.5.5

...

...

exercises ready

all ex done

...

....

fixed

removed some printings

commented out unfinished proof

removed some printings

better spacing

apply rule (lem EM) works

missing subst added, now apply rule is probably enough to replace apply

New bug.

no more prove in palette

fixed or-in-left

fixed not-e

Another bug.

This commit shows a bug.

almost ready

rules fixed

make all/clean implemented

housekeeping

housekeeping

house keeping

disambiguation can use a goal as hint for the expected type

natural deduction palette

test 4 luo

...

better names

disambiguation for ng terms almost there

some new exports

new meta added for ng_disambiguation

exported disambiguate_thing

occurr check fixed

more printings

last fixes

1. data structure for lables is now more strict
2. phase 3 completed (with a test)
3. simple optimizer for redundant jumps implemented

- we now use a streaming architecture (run time gain: 11 secs)
- we added some time stamp support

auto-param "size" missing

debug=false

Signature_of has been closed with respect to constructors.

The signature in "retrieve equations" must be extended with the equality if
not already there, otherwise it may hardly find any equation.

some other simplification

ordered_set simplified

exercise ready

exercise ready

almost there

...

First attempts at the third phase.

added some news

almost ok

natural deduction support and example split, seems to almost work.

do not erase sorts

better error messages. sorts are compared using whd

Evil case fixed, the coulde should be more readable

removed empty lines

the passive set and passive list are expected to have the same cardinality, that was was some bad reason not always the case

fixed scripts

still some glitches, but reaching a decent state

using the new by foo we proved semantics

new internal flags for auto:
- skip_context
- skip_trie_filtering

together they allow a decent semantics for
by H, H1, H2 we proved foo.

since only H, H1 and H2 are used (no other context entry, not library stuff)
and full blown unification is used (no terms are ignored, between the one
specified, because they fail a trie search)

duplicate entry in menv avoided

fixed script to use auto depth=4

eliminazione di un passaggio di transitività in ast2astfe
dimostrazione di un assioma in env2flatenv

Calling unification instead of matching when checking for subsumption
might instantiate the goal with variables in table (while they are supposed
to be disjoint).

- A new interesting elimination principle over inductively generated topologies:
  the elimination principle for general topologies hold!
- A proof of Cantor theorem using formal topologies. By Silvio Valentini.

BDD

removed prerr_endline

debug=false

shannon proved

added shannon

added lazy

Environment simplified.

No longer used.

- New dependency for environments on the nesting depth.
- New invariant that tightly binds the list of identifiers in scope with
  the list of mappings in an environment transformation map
- Second pass of the compiler finally complited

Propagation of changes in paramodulation.

Exported a couple of functions.
--Thi sline, and those below, will be ignored--

M    metadataQuery.mli

Added a in_universe function

propagation of changes in other paramodulation files.

New demod function working for arbitary goals.

models ported

Enforcing the disjoint invariant between metasenvs.

Main change: added a parameter to build_equality_proof to discriminate
bewteen forward and backward rewriting steps.