aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2020-03-02 16:29:51 +0100
committerPierre-Marie Pédrot2020-05-11 13:24:50 +0200
commitead129a76cb3ceb656b60556bf10f38c667ce45a (patch)
treea16633b2a9bb11c0b35a5fc07b4ae288deece873 /kernel
parent457cee4345ab4ad6b6624a6886841fd0b0739b2a (diff)
Generalize the Ltac2 value criterion to pure let-bindings.
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions