aboutsummaryrefslogtreecommitdiff
path: root/kernel/nativelambda.ml
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2021-03-06 23:32:45 +0100
committerPierre-Marie Pédrot2021-03-12 13:39:03 +0100
commit285419e99996354ad2056bc38725c7a592124e7c (patch)
treee4501ef5d6ccfa34643fde049e98fd156830bf54 /kernel/nativelambda.ml
parent93ea9206cbf29617feb23646f95e794b11e87793 (diff)
Further simplification of the term replacing code.
We factorize the code for replace and subst, since it seems there is no reason to keep them separate, not even performance. Some static invariants are made explicit in the API.
Diffstat (limited to 'kernel/nativelambda.ml')
0 files changed, 0 insertions, 0 deletions