diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-12-05 12:04:14 -0500 |
|---|---|---|
| committer |  Jason Gross <jasongross9@gmail.com> | 2018-01-29 18:04:58 -0500 |
| commit | 35d68e63e24d01598c23a269a1d1e1de41e213ab (patch) | |
| tree | 0abca08d02e32449b505292d4d4157a85eb8d9a4 /src | |
| parent | c88faab0f5e036123bafcc0349a35f76d750b564 (diff) | |
Add a reference to a Coq issue
Diffstat (limited to 'src')
| -rw-r--r-- | src/Experiments/SimplyTypedArithmetic.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Experiments/SimplyTypedArithmetic.v b/src/Experiments/SimplyTypedArithmetic.v index 8fef7530d..d9099021f 100644 --- a/src/Experiments/SimplyTypedArithmetic.v +++ b/src/Experiments/SimplyTypedArithmetic.v @@ -616,7 +616,7 @@ Module Compilers. => Some v | _ => None end. - (* oh, the horrors of not being able to use non-linear deep pattern matches *) + (* oh, the horrors of not being able to use non-linear deep pattern matches. c.f. COQBUG(https://github.com/coq/coq/issues/6320) *) Fixpoint invert_list_full {t} (e : @expr var (type.list t)) : option (list (@expr var t)) := match e in expr t return option match t with |