-
Robbert Krebbers authored
Otherwise, whenever it cannot establish the Absorbing or Affine premise, it will backtrack on the FromAssumption premise, causing a possible loop. No idea why this happens, this may be a Coq bug...
5599f3d1
Otherwise, whenever it cannot establish the Absorbing or Affine premise, it will backtrack on the FromAssumption premise, causing a possible loop. No idea why this happens, this may be a Coq bug...