• Guillaume Melquiond's avatar
    Switch to an always-on realization mode for Coq. · f796cd6d
    Guillaume Melquiond authored
    There are hardly any change to the code. It now just looks whether
    dependencies are marked as realized. The old no-realization mode is
    equivalent to marking no theory as realized, while the old realization
    mode amounts to marking all of the theories as realized. Now, the finer
    granularity make any intermediate state reachable. This is just a proof
    of concept, so the actual set of realized theories is hard-coded.
coq.ml 25.8 KB