diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-04-01 18:37:50 -0400 |
|---|---|---|
| committer |  Jason Gross <jasongross9@gmail.com> | 2017-04-02 10:27:49 -0400 |
| commit | 83d035c40eb8f4f66097c003f90fab0a58fa25d8 (patch) | |
| tree | c82b74b80e511d9afcf32b5abc8d2fb05a05b199 /src/Experiments/Ed25519_imports.hs | |
| 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/Experiments/Ed25519_imports.hs')
0 files changed, 0 insertions, 0 deletions