Transfers to checker ("let"s in inductive arities + Coq root read-only).

- Support for let's in the signature of the arity of an inductive type was
  in the kernel part of commit 12273,
- Support for binding Coq root read-only in -R option was in commit 12220.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12288 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 0 insertions, 7 deletions

diff --git a/checker/checker.ml b/checker/checker.ml
index b982456aa..85ad129c9 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -90,23 +90,16 @@ let includes = ref []
 let push_include (s, alias) = includes := (s,alias,false) :: !includes
 let push_rec_include (s, alias) = includes := (s,alias,true) :: !includes
 
-let check_coq_overwriting p = 
-  if string_of_id (list_last (repr_dirpath p)) = "Coq" then
-    error "The \"Coq\" logical root directory is reserved for the Coq library"
-
 let set_default_include d =
   push_include (d, Check.default_root_prefix)
 let set_default_rec_include d =
   let p = Check.default_root_prefix in
-  check_coq_overwriting p; 
   push_rec_include (d, p)
 let set_include d p =
   let p = dirpath_of_string p in
-  check_coq_overwriting p;
   push_include (d,p)
 let set_rec_include d p =
   let p = dirpath_of_string p in
-  check_coq_overwriting p;
   push_rec_include(d,p)
 
 (* Initializes the LoadPath *)