diff options
| author | Emilio Jesus Gallego Arias | 2020-03-10 18:14:07 -0400 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-03-10 18:14:07 -0400 |
| commit | 98b25745ab50df8f5f263cd32dbe8525aa525ea8 (patch) | |
| tree | 9e8374164ef57776fb0df08bb6bf96259db5a0b2 /lib | |
| parent | 4cc3f613c96197dd9e6b5f531fa4c68968f27176 (diff) | |
| parent | 9c2092b456c4ad56e2b680e700080355fc652a6b (diff) | |
Merge PR #11767: Fix #11738 : Funind using deprecated Coqlib API.
Reviewed-by: ejgallego
Reviewed-by: maximedenes
Diffstat (limited to 'lib')
0 files changed, 0 insertions, 0 deletions