scopedTerm.bij
functorized type
functorizing symbol (in progress)
smallish Interface
.Seq module in FOTerm and FOFormula to iterate on subterms, vars, symbols, etc. in
a more general and composable way;
subsequently modified several functions to use those iterators
Util.list_fold_product
typo
merge from dev
downcasting function in Type (from general term to type)
Merge branch 'dev' into common_term
merge from dev
transient state (dnc), with better Type and ScopedTerm, but stuck Symbol;
Several implems of Symbol is too complicated, and only one should be used;
hashconsed Symbol but without global/mutable state (use hashtable+variants for properties)
use Zarith
.merlin
use a single representation for Symbol, much much much simpler;
it has a variant for connectives, syntax-independent (syntaxes should provide their own printers);
Type is a subtype of ScopedTerm.Std.t (instance of ScopedTerm for Symbol)
merge bugfix from master
simplified again ScopedTerm (no more functor)
renamed variants of Symbol.t
updated Type to use ScopedTerm.t
ScopedTerm explicitely uses Symbol; exports tType (which is its own type)