diff options
author | 2017-04-01 18:37:50 -0400 | |
---|---|---|
committer | 2017-04-02 10:27:49 -0400 | |
commit | 83d035c40eb8f4f66097c003f90fab0a58fa25d8 (patch) | |
tree | c82b74b80e511d9afcf32b5abc8d2fb05a05b199 /src/SpecificGen/GF5211_32ExtendedAddCoordinates.v | |
parent | d5006369495a4e79c4db011d8fdb334b266381f2 (diff) |
Work around bug #5434
This is https://coq.inria.fr/bugs/show_bug.cgi?id=5434, [vm_compute]
breaks an invariant asserted on line 115 of
pretyping/constr_matching.ml. This was triggering whenever we tried to
reify one of the operations.
Diffstat (limited to 'src/SpecificGen/GF5211_32ExtendedAddCoordinates.v')
0 files changed, 0 insertions, 0 deletions