draft of Extensions, with dynamic plugins;
CLI option to load plugins in zipperposition
update of the Makefile: removed Batteries, added Dynlink;
cleaned the targets, factored out with a TAGS variable;
added a target to compile plugins
search for plugins as .cmxs files, but also in the standard plugins dir
cosmetic changes
more recent version of containers (with CC, Puf...)
added stuff for congruence closure and semantic tautology deletion (disabled, does not seem useful for now)
small set data structure (sorted list)
refactored Index, with polymorphic object signatures;
also, Index.unit_t (rewriting index) can be built from a regular index
Makefile target for building only tests
new module, FoSubst.Renaming, used to rename free
variables without ambiguities when a substitution is applied; lits and clauses use it
refactoring of indexes, to make them polymorphic
?renaming is optional in FoSubst.apply_subst; if not
provided, the old behavior (shifting) is used (more efficient in many cases)
update lib.mllib with more modules
finished the refactoring of indexes, in all the modules that use them;
also updated those modules to use the new substitutions/renaming
immutable records for precedence and ordering;
context is now updatable in place to change the ordering
more recent version of containers
smallSet is an increasing list
updated clauses to use a SmallSet for descendants;
refactored ClauseQueues without objects;
minor changes (Clauses.CSet uses a Map for ints rather than Ptmap)
big refactoring: use new module Env, with value Env.t, to carry all the stateful
stuff the prover needs (well, almost all), including params, state, inference/simplification rules, context;
use a modular interface to use this Env.t;
updated Saturate and Zipperposition to use this new Env (removed Calculus)
rewritten extensions system; Extensions can register actions to an Env.t, like
inference rules, experts or simplification rules