aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker/include
diff options
context:
space:
mode:
authorGravatar Bruno Barras <bruno.barras@inria.fr>2014-11-27 17:01:58 +0100
committerGravatar Bruno Barras <bruno.barras@inria.fr>2015-01-06 15:32:12 +0100
commited93de78345ecd93c4fd8cac0917f1fd34f51d44 (patch)
tree88adafc154a9c455ff333b42d8cceb505017e347 /checker/include
parent5b1e6e58235e8f3fdf6f49329adbd6e9b014fd78 (diff)
improve efficiency of the reduction interpreter of coqtop
Conflicts: kernel/closure.ml kernel/closure.mli kernel/reduction.ml
Diffstat (limited to 'checker/include')
0 files changed, 0 insertions, 0 deletions