diff options
| author | Pierre Courtieu | 2020-03-05 19:31:18 +0100 |
|---|---|---|
| committer | Pierre Courtieu | 2020-03-06 16:58:59 +0100 |
| commit | 9c2092b456c4ad56e2b680e700080355fc652a6b (patch) | |
| tree | 12a09c9b94b725de5323ec264014de8f6936129d /lib | |
| parent | 56b6e41c162f1aabd9e17ace7ceeab9afd556fe4 (diff) | |
Fix #11738 : Funind using deprecated Coqlib API.
Diffstat (limited to 'lib')
0 files changed, 0 insertions, 0 deletions