• Andrei Paskevich's avatar
    Subst: avoid selecting polymorphic symbols and constructors · f542a3e4
    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
Makefile.in 74.9 KB