-
Andrei Paskevich authored
Also, add an .mli file and export the relevant functions. Also, provide a variant of "split_vc" in introduction.ml which uses subst over introduced non-model constants instead of "simplify_trivial_quantification". This is more efficient and produces better results. Commented at the moment because of session breakage.
f542a3e4