aboutsummaryrefslogtreecommitdiff
path: root/pretyping/program.ml
diff options
context:
space:
mode:
authorcoqbot-app[bot]2021-03-31 06:31:36 +0000
committerGitHub2021-03-31 06:31:36 +0000
commit6b5102bad5a75ede001908709f0b159127887667 (patch)
tree0ff54db09d96d5a93f88025d32384f9a8834b1c2 /pretyping/program.ml
parent4eb219067baa0f9ea806794d242de13c3a3a2826 (diff)
parent58f35aad952c94744f232b622ab07ffb5d932a15 (diff)
Merge PR #14022: Replace mentions of Num by Zarith.
Reviewed-by: pi8027
Diffstat (limited to 'pretyping/program.ml')
0 files changed, 0 insertions, 0 deletions