diff options
| author | herbelin | 2013-06-02 21:31:26 +0000 |
|---|---|---|
| committer | herbelin | 2013-06-02 21:31:26 +0000 |
| commit | 164b3bdb69f60b9bbbe83abce73c6256869d1f4b (patch) | |
| tree | b66508896a009c951fc5b83f4a40f027eccaa892 | |
| parent | 1b2a6326876c67bf25657ecd7c0765cacd1cde75 (diff) | |
Modest protection against "injection" and co raising anomaly in
-nois mode. This is not perfect yet. E.g. "injection" used while
before eq is defined while compiling Logic.v would raise an anomaly.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16548 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | interp/coqlib.ml | 12 |
1 files changed, 9 insertions, 3 deletions
diff --git a/interp/coqlib.ml b/interp/coqlib.ml index 34ea7b607d..3a041a27f5 100644 --- a/interp/coqlib.ml +++ b/interp/coqlib.ml @@ -83,11 +83,17 @@ let check_required_library d = (************************************************************************) (* Specific Coq objects *) -let init_reference dir s = gen_reference "Coqlib" ("Init"::dir) s +let init_reference dir s = + let d = "Init"::dir in + check_required_library ("Coq"::d); gen_reference "Coqlib" d s -let init_constant dir s = gen_constant "Coqlib" ("Init"::dir) s +let init_constant dir s = + let d = "Init"::dir in + check_required_library ("Coq"::d); gen_constant "Coqlib" d s -let logic_constant dir s = gen_constant "Coqlib" ("Logic"::dir) s +let logic_constant dir s = + let d = "Logic"::dir in + check_required_library ("Coq"::d); gen_constant "Coqlib" d s let arith_dir = ["Coq";"Arith"] let arith_modules = [arith_dir] |