diff options
| author | coqbot-app[bot] | 2021-03-31 06:31:36 +0000 |
|---|---|---|
| committer | GitHub | 2021-03-31 06:31:36 +0000 |
| commit | 6b5102bad5a75ede001908709f0b159127887667 (patch) | |
| tree | 0ff54db09d96d5a93f88025d32384f9a8834b1c2 /Makefile.dev | |
| parent | 4eb219067baa0f9ea806794d242de13c3a3a2826 (diff) | |
| parent | 58f35aad952c94744f232b622ab07ffb5d932a15 (diff) | |
Merge PR #14022: Replace mentions of Num by Zarith.
Reviewed-by: pi8027
Diffstat (limited to 'Makefile.dev')
0 files changed, 0 insertions, 0 deletions