diff options
| author | Guillaume Melquiond | 2021-03-28 17:12:49 +0200 |
|---|---|---|
| committer | Guillaume Melquiond | 2021-03-28 17:12:49 +0200 |
| commit | 58f35aad952c94744f232b622ab07ffb5d932a15 (patch) | |
| tree | 171ecec960809ed5ca7ef93eeaa3e0cf6a849a31 /plugins | |
| parent | e414d25f120696dbd1956b230801d22810746f58 (diff) | |
Replace mentions of Num by Zarith.
The documentation of extraction became outdated when the big.ml wrapper
got modified by 094e4649c29e2426daca0476c140439de901dafe.
Diffstat (limited to 'plugins')
0 files changed, 0 insertions, 0 deletions