diff options
| author | Vincent Laporte | 2019-02-26 17:53:34 +0000 |
|---|---|---|
| committer | Vincent Laporte | 2019-02-26 17:53:34 +0000 |
| commit | 4610afafcbd79f38876e528c0f30c9347648efc4 (patch) | |
| tree | a124c070d37ae3af56156f6b92764ae46ff8f87c /vernac/comProgramFixpoint.ml | |
| parent | 9d6f268723b6352a97bcc3baf0df57f1c1b251fa (diff) | |
| parent | 4d209729a78d7d8ec24d7b6b5a45460aff36a195 (diff) | |
Merge PR #9612: Fix #9526: Registering inductives for primitive integers doesn't check enough
Ack-by: SkySkimmer
Reviewed-by: vbgl
Diffstat (limited to 'vernac/comProgramFixpoint.ml')
0 files changed, 0 insertions, 0 deletions