diff options
| author | letouzey | 2011-09-23 11:27:46 +0000 |
|---|---|---|
| committer | letouzey | 2011-09-23 11:27:46 +0000 |
| commit | 99673b71ac2d0e8ff81d58ee8f1ded888531c86f (patch) | |
| tree | fbb1e2b4402e97e943bbb1359d20fcfc22183de1 /kernel/typeops.ml | |
| parent | 39bc0059d2730961c48b99a007127804d9fe2122 (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 'kernel/typeops.ml')
0 files changed, 0 insertions, 0 deletions