aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
authorletouzey2011-09-23 11:27:46 +0000
committerletouzey2011-09-23 11:27:46 +0000
commit99673b71ac2d0e8ff81d58ee8f1ded888531c86f (patch)
treefbb1e2b4402e97e943bbb1359d20fcfc22183de1 /dev
parent39bc0059d2730961c48b99a007127804d9fe2122 (diff)
Program: add some check_required_library (fix #2592) + some dead code removal
If these additional checks take too much time, maybe using true laziness instead of (fun () -> ...) could help. Btw, some other init_constant in Program would deserve preliminary check_required_library... I've also removed some unused delayed constr, at least one of them being erroneous git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14489 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions