diff options
| author |  Yves Bertot <Yves.Bertot@inria.fr> | 2016-10-24 08:48:05 +0200 |
|---|---|---|
| committer |  Maxime Dénès <mail@maximedenes.fr> | 2016-10-25 09:39:16 +0200 |
| commit | a7996005f57c12ba8fbb22c61ad97ac872da9d83 (patch) | |
| tree | 1d2d479a31417cf4c4bf07552061f85dda89c029 /kernel/byterun/coq_instruct.h | |
| parent | 46462c3cc69e97bf3260f1aad5faaa6eaf6c2722 (diff) | |
That Function is unable to create a Fixpoint equation is a user problem,
not an anomaly
Diffstat (limited to 'kernel/byterun/coq_instruct.h')
0 files changed, 0 insertions, 0 deletions