aboutsummaryrefslogtreecommitdiff
path: root/kernel/nativelambda.mli
diff options
context:
space:
mode:
authorPaul Steckler2016-08-17 17:14:55 -0400
committerPaul Steckler2016-08-17 17:45:00 -0400
commit982e239e2befe925410a08459053c7dc69c948a7 (patch)
tree0a2fb48000de643bbee7cbcb9c46211ab24c829c /kernel/nativelambda.mli
parentd1052e2d9e14684db1f86a9b419d388a8e70728c (diff)
In docs, fix command to reset Ltac profiling
Diffstat (limited to 'kernel/nativelambda.mli')
0 files changed, 0 insertions, 0 deletions