diff --git a/src/ecLoader.ml b/src/ecLoader.ml
index 25378c19e..b52f663c2 100644
--- a/src/ecLoader.ml
+++ b/src/ecLoader.ml
@@ -26,6 +26,11 @@ let getkind ext =
   | "eca" -> `EcA
   | _     -> raise (BadExtension ("." ^ ext))
 
+let string_of_namespace ns = 
+  match ns with
+  | `System -> "System"
+  | `Named s -> s
+
 (* -------------------------------------------------------------------- *)
 let create () = { ecl_idirs = []; }
 
diff --git a/src/ecLoader.mli b/src/ecLoader.mli
index 3b5fe2d31..2338f6ad7 100644
--- a/src/ecLoader.mli
+++ b/src/ecLoader.mli
@@ -12,6 +12,8 @@ val getkind : string -> kind
 (* -------------------------------------------------------------------- *)
 type namespace = [ `System | `Named of string ]
 
+val string_of_namespace : namespace -> string
+
 (* -------------------------------------------------------------------- *)
 val create  : unit -> ecloader
 val aslist  : ecloader -> ((namespace option * string) * idx_t) list
diff --git a/src/ecScope.ml b/src/ecScope.ml
index 77325401d..4403502f6 100644
--- a/src/ecScope.ml
+++ b/src/ecScope.ml
@@ -1816,12 +1816,22 @@ module Theory = struct
         sc_env = EcSection.add_th ~import cth scope.sc_env }
 
   (* ------------------------------------------------------------------ *)
-  let required (scope : scope) (name : required_info) =
+  let required (scope : scope) (rqd : required_info) =
     assert (scope.sc_pr_uc = None);
     List.exists (fun x ->
-        if x.rqd_name = name.rqd_name then (
-          (* FIXME: raise an error message *)
-          assert (x.rqd_digest = name.rqd_digest);
+        if x.rqd_name = rqd.rqd_name then (
+          if (x.rqd_digest <> rqd.rqd_digest) then begin
+            let fullname (ri : required_info) =
+              let namespace =
+                ri.rqd_namespace
+                |> Option.map EcLoader.string_of_namespace
+                |> Option.map (fun s -> s ^ ":")
+                |> Option.value ~default:"" in
+              namespace ^ ri.rqd_name in
+            hierror
+              "Digest mismatch, file %s differs from %s"
+              (fullname x) (fullname rqd)
+          end;
           true)
         else false)
       scope.sc_required
diff --git a/tests/require_test/easycrypt.project b/tests/require_test/easycrypt.project
new file mode 100644
index 000000000..ff9bcb9f5
--- /dev/null
+++ b/tests/require_test/easycrypt.project
@@ -0,0 +1,6 @@
+[general]
+provers = CVC5@1.0
+provers = Z3@4.12
+
+idirs=Foo2:foo2
+idirs=Foo1:foo1
diff --git a/tests/require_test/foo1/main.ec b/tests/require_test/foo1/main.ec
new file mode 100644
index 000000000..072e1ab23
--- /dev/null
+++ b/tests/require_test/foo1/main.ec
@@ -0,0 +1,7 @@
+require import AllCore Int Real.
+
+op foo : real = 1%r.
+
+theory A.
+  op add : real -> real -> real = (+)%r.
+end A.
diff --git a/tests/require_test/foo2/main.ec b/tests/require_test/foo2/main.ec
new file mode 100644
index 000000000..60b3fd730
--- /dev/null
+++ b/tests/require_test/foo2/main.ec
@@ -0,0 +1,9 @@
+require import AllCore Int.
+
+op foo : int = 2.
+
+op foo2 : int = 3.
+
+theory A.
+  op add : int -> int -> int = (-).
+end A.
diff --git a/tests/require_test/main.ec b/tests/require_test/main.ec
new file mode 100644
index 000000000..072e1ab23
--- /dev/null
+++ b/tests/require_test/main.ec
@@ -0,0 +1,7 @@
+require import AllCore Int Real.
+
+op foo : real = 1%r.
+
+theory A.
+  op add : real -> real -> real = (+)%r.
+end A.
diff --git a/tests/require_test/require.ec b/tests/require_test/require.ec
new file mode 100644
index 000000000..c986b4bc0
--- /dev/null
+++ b/tests/require_test/require.ec
@@ -0,0 +1,3 @@
+from Foo2 require import Main.
+fail require import Main.
+fail from Foo1 require import Main.