• Paolo G. Giarrusso's avatar
    Switch `inj _` to `inj f`, part 2 · ffa05e8a
    Paolo G. Giarrusso authored
    Code not affected by a00d9bd8.
    
    All occurrences are gone, except for one in `base.v` where you'd need different
    functions.
    
    However, I'm unsure this is an improvement: in lots of cases here, the function
    didn't need to be guessed, but could be deduced by "simple" higher-order
    unification, the one where unifying `?f ?a` against `g args last_arg` sets `?f =
    g args`.
    ffa05e8a
gmultiset.v 21.5 KB