-
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.
Raphaël Cauderlier authoredThe 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