aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/himsg.ml
diff options
context:
space:
mode:
authorGravatar Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>2018-02-02 14:11:33 +0100
committerGravatar Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>2018-02-02 14:41:23 +0100
commit1d9e15c99a90311f8e082fb39615ae1c4aee8084 (patch)
tree83774712b333ff1ebdaf805da0d02be816f9790d /vernac/himsg.ml
parentc9839e30e1b46e70c85533d95e4f4cc2ae826c66 (diff)
checker: cleanup projection unfolding
This just shares the unfold_projection between Closure and Reduction.
Diffstat (limited to 'vernac/himsg.ml')
0 files changed, 0 insertions, 0 deletions