• Guillaume Melquiond's avatar
    Fix Coq files after removal of axioms. · 1e29247f
    Guillaume Melquiond authored
    Somehow they went under the radar the first time. Now all of them should
    have been fixed.
    Strangely enough, as can be seen from the diff, the statement of
    WP_parameter_gcd was thoroughly wrong. The old proof was actually matching
    the new statement, so the file would never have compiled on its own. I
    don't have any sensible explanation for such a breakage, except for gnomes
    messing with bytes at night.
gcd_bezout_WP_GcdBezout_WP_parameter_gcd_1.v 5.55 KB