diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-06-15 12:53:01 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-06-17 11:38:47 +0200 |
| commit | abd89e37c2882e0f92a3e119b4eb7ee44cc8a503 (patch) | |
| tree | 6432e7b5e0fad15dddcd7aeda86ba199c15d0557 /pretyping/indrec.mli | |
| parent | d62354b7e9ff8e20aa959984b392a27e26f9fc24 (diff) | |
Fixes #7811 (uncaught Not_found in notation printer related to "match").
Diffstat (limited to 'pretyping/indrec.mli')
0 files changed, 0 insertions, 0 deletions