aboutsummaryrefslogtreecommitdiff
path: root/kernel/nativelambda.ml
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2020-06-29 13:39:18 +0200
committerEmilio Jesus Gallego Arias2020-07-08 15:12:46 +0200
commit301e9cb85c2ac995d71cb7978ceae78621ec3eee (patch)
tree9699c7933b193019c61e21ce7f90b7c4838b641b /kernel/nativelambda.ml
parent54788df72ce79998ee27db362401a56bda4daceb (diff)
[obligations] Remove duplicate progmap_remove.
This is already taken of by `declare_definition`, by consistency with the mutual case.
Diffstat (limited to 'kernel/nativelambda.ml')
0 files changed, 0 insertions, 0 deletions