GitLab

Avoid inlining proxy variables whenever there are conflicting effects

Not inlining proxy variables inside a [Efun].

Extraction of let x = e1 in e2

Fold_left for lists and sequences (wip)

Not printing parentheses around constants
(though still not completely satisfying

Optimization of proxy variables.

Why3 files from standard library are not extracted

Optimization of singleton record types.
Still missing treatment of record types defined in drivers

Preparing for the GT demo

Empty extracted modules (all definitions are defined in the driver)
are printed no more, independently of the extraction mode

New command line nearly done

Preparing for the new command line.

Preparing for the new command line (flat recursive extraction of symbols
only works for definitions in the same file).

Preparing for the new command line (not working for now).

Preparing for the new command line.

Preparation for the new command line

Preparation for the new command line

Preparing for monolithic extraction.

Better treatment of partial applied constructors

in preparation of command-line option --mono