aboutsummaryrefslogtreecommitdiff
path: root/kernel/nativelambda.ml
diff options
context:
space:
mode:
authorcoqbot-app[bot]2021-01-28 21:20:59 +0000
committerGitHub2021-01-28 21:20:59 +0000
commited29e0913742c307175846557ed8390a8da771e3 (patch)
treee086e1cecc69e532686cf6d6c3de8a422638e6f5 /kernel/nativelambda.ml
parent59dc4eb40e9512d95f73df7a6bc67edcb1907acd (diff)
parentde7f7fe34828debfa4bd5130810ee5ccc0ea0170 (diff)
Merge PR #13789: Document limitation of rewrite regarding occurrence selection.
Reviewed-by: jfehrle Reviewed-by: silene
Diffstat (limited to 'kernel/nativelambda.ml')
0 files changed, 0 insertions, 0 deletions