diff options
| author | Pierre-Marie Pédrot | 2020-10-27 13:31:44 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-10-27 13:31:44 +0100 |
| commit | b87fd6cfe5fe872a38d98c294aea84cde8c6c160 (patch) | |
| tree | 060327d404f1e9fcf198aff8d5f075ec498f261e /kernel/nativecode.ml | |
| parent | 82f7cc4a408cf100fda43139c0b1d33e33748799 (diff) | |
| parent | 30f97beb1bfc149d9608cb74f24f69f268671e04 (diff) | |
Merge PR #13167: Ltac2: use ComTactic infrastructure
Reviewed-by: ejgallego
Reviewed-by: gares
Reviewed-by: ppedrot
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions