From 164b3bdb69f60b9bbbe83abce73c6256869d1f4b Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 2 Jun 2013 21:31:26 +0000
Subject: 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
---
 interp/coqlib.ml | 12 +++++++++---
 1 file 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]
-- 
cgit v1.2.3