diff options
| author | Clément Pit-Claudel | 2019-05-20 16:04:34 -0400 |
|---|---|---|
| committer | Clément Pit-Claudel | 2020-03-19 13:51:06 -0400 |
| commit | 9280fdd8f1eb05f4823e0436b629c8ec4716f326 (patch) | |
| tree | ce1ce685884cb225b734b06aa6dd681634f43f80 /vernac/comProgramFixpoint.ml | |
| parent | 9492db6eeab7c8d29d7f4374fdbafe659149b231 (diff) | |
[refman] Stop using the deprecated math_block node (fixed GH-11856)
Diffstat (limited to 'vernac/comProgramFixpoint.ml')
0 files changed, 0 insertions, 0 deletions