Skip to content
  • Raphaël Cauderlier's avatar
    f48ea1e0
    [michocoq] avoid reasoning on dependent if · f48ea1e0
    Raphaël Cauderlier authored
    The dependent if construction error.dif wasn't very convenient because
    Coq was rarely able to infer the implicit type predicate
    parameter. This commit drops it in favor of a simpler construction
    error.assume that can be used while working inside the error monad to
    check that a boolean is true and obtain a witness of this fact.
    f48ea1e0
    [michocoq] avoid reasoning on dependent if
    Raphaël Cauderlier authored
    The dependent if construction error.dif wasn't very convenient because
    Coq was rarely able to infer the implicit type predicate
    parameter. This commit drops it in favor of a simpler construction
    error.assume that can be used while working inside the error monad to
    check that a boolean is true and obtain a witness of this fact.
Loading