aboutsummaryrefslogtreecommitdiff
path: root/doc/stdlib/Library.tex
diff options
context:
space:
mode:
authorBruno Barras2014-11-27 17:01:58 +0100
committerBruno Barras2015-01-06 15:32:12 +0100
commited93de78345ecd93c4fd8cac0917f1fd34f51d44 (patch)
tree88adafc154a9c455ff333b42d8cceb505017e347 /doc/stdlib/Library.tex
parent5b1e6e58235e8f3fdf6f49329adbd6e9b014fd78 (diff)
improve efficiency of the reduction interpreter of coqtop
Conflicts: kernel/closure.ml kernel/closure.mli kernel/reduction.ml
Diffstat (limited to 'doc/stdlib/Library.tex')
0 files changed, 0 insertions, 0 deletions