[coq_lib] Enforce that boot libraries depend on no theories

Signed-off-by: Emilio Jesus Gallego Arias <e+git@x80.org>

src/dune_rules/coq_lib.ml

@@ -123,6 +123,7 @@ module Error = struct
       [ Pp.textf "Cannot have more than one boot theory in scope:"
       ; Pp.enumerate theories ~f:name
       ]
+
 end
 
 let top_closure =

src/dune_rules/coq_stanza.ml

@@ -83,6 +83,7 @@ module Extraction = struct
 end
 
 module Theory = struct
+
   type t =
     { loc : Loc.t
     ; name : Coq_lib_name.t
@@ -133,6 +134,9 @@ module Theory = struct
              1.0 version of the Coq language"
         ]
 
+  let boot_has_deps () =
+    User_error.raise [ Pp.textf "(boot) libraries cannot have dependencies" ]
+
   let decode =
     fields
       (let+ loc, name = field "name" Coq_lib_name.decode
@@ -145,6 +149,8 @@ module Theory = struct
        and+ modules = Stanza_common.modules_field "modules"
        and+ enabled_if = Enabled_if.decode ~allowed_vars:Any ~since:None ()
        and+ buildable = Buildable.decode in
+       (* boot libraries cannot depend on other theories *)
+       if boot && List.is_non_empty buildable.theories then boot_has_deps ();
        let package = select_deprecation ~package ~public in
        { loc
        ; name