diff options
| author | Hugo Herbelin | 2020-03-04 21:35:49 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-03-04 21:35:49 +0100 |
| commit | 33ab70ac3a8d08afb67d9602d7c23da7133ad0f4 (patch) | |
| tree | 7159a39d683a05e4239ac3a0d50dd20eb8d6719b /plugins/micromega/persistent_cache.ml | |
| parent | cfecd54efac7191690f37af1edcc91389ae180e1 (diff) | |
| parent | 54562510ed05bacdf7c9c2a41bb104a68aeaa1c0 (diff) | |
Merge PR #11715: Be robust in calculating visible ids for non-registered constants.
Reviewed-by: herbelin
Diffstat (limited to 'plugins/micromega/persistent_cache.ml')
0 files changed, 0 insertions, 0 deletions