diff options
| author | Emilio Jesus Gallego Arias | 2019-06-16 14:50:38 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-06-16 14:50:38 +0200 |
| commit | 6eba5b5ba91f9ec02b809e0c223324e0f4fdbf85 (patch) | |
| tree | 3914740835572b424500576e11fe6e4e1fac1ba4 /kernel/nativelibrary.ml | |
| parent | 5d58496c27fc5767c7841734c0f01a739cf529ab (diff) | |
| parent | 27b6f605efb2e94656c3405ddc271a775fbdab7e (diff) | |
Merge PR #10345: Fix #10339: Anomaly in Ltac2.
Reviewed-by: ejgallego
Diffstat (limited to 'kernel/nativelibrary.ml')
0 files changed, 0 insertions, 0 deletions