diff --git a/src/ecCoreModules.ml b/src/ecCoreModules.ml
index 891e897e2..eb202d64e 100644
--- a/src/ecCoreModules.ml
+++ b/src/ecCoreModules.ml
@@ -553,6 +553,18 @@ type top_module_expr = {
 let is_me_body_alias (body : module_body) =
   match body with ME_Alias _ -> true | _ -> false
 
+let module_own_state (me : module_expr) : symbol list option =
+  let rec for_comps (comps : module_comps) : symbol list option =
+    List.opick for_item comps
+
+  and for_item (item : module_item) : symbol list option =
+    match item with
+    | MI_Variable v -> Some [v.v_name]
+    | MI_Function _ -> None
+    | MI_Module  me -> omap (fun p -> me.me_name :: p) (for_comps me.me_comps)
+
+  in for_comps me.me_comps
+
 (* -------------------------------------------------------------------- *)
 let ur_hash = EcAst.ur_hash
 
diff --git a/src/ecCoreModules.mli b/src/ecCoreModules.mli
index 69b7a3753..060fc4756 100644
--- a/src/ecCoreModules.mli
+++ b/src/ecCoreModules.mli
@@ -257,6 +257,10 @@ type top_module_expr = {
 
 val is_me_body_alias : module_body -> bool
 
+(* Component path of the first program variable owned by the module, [None] if
+   it owns none (transitively through its sub-modules). *)
+val module_own_state : module_expr -> symbol list option
+
 (* -------------------------------------------------------------------- *)
 val mty_equal :
   module_type ->
diff --git a/src/ecParser.mly b/src/ecParser.mly
index 9552a74a1..1be4a3f7a 100644
--- a/src/ecParser.mly
+++ b/src/ecParser.mly
@@ -3911,11 +3911,8 @@ clone_override:
 | LEMMA x=qoident mode=loc(opclmode) y=qoident
   { x, PTHO_Axiom (y, unloc mode) }
 
-| MODULE uqident loc(opclmode) uqident
-   { parse_error
-       (EcLocation.make $startpos $endpos)
-       (Some "Module overriding is no longer supported.")
-   }
+| MODULE x=uqident mode=loc(opclmode) y=uqident
+   { (x, PTHO_Module (y, unloc mode)) }
 
 | MODULE TYPE x=uqident mode=loc(opclmode) y=uqident
    { (x, PTHO_ModTyp (y, unloc mode)) }
diff --git a/src/ecParsetree.ml b/src/ecParsetree.ml
index 2a70a2e92..51e62a89c 100644
--- a/src/ecParsetree.ml
+++ b/src/ecParsetree.ml
@@ -1359,6 +1359,7 @@ and theory_override =
 | PTHO_Op     of op_override
 | PTHO_Pred   of pr_override
 | PTHO_Axiom  of ax_override
+| PTHO_Module of me_override
 | PTHO_ModTyp of mt_override
 | PTHO_Theory of th_override
 
diff --git a/src/ecReduction.ml b/src/ecReduction.ml
index 036648e58..9f39592b3 100644
--- a/src/ecReduction.ml
+++ b/src/ecReduction.ml
@@ -343,6 +343,9 @@ end) = struct
   let rec for_module_expr env ~norm ~body me1 me2 =
     me1.me_name = me2.me_name &&
       for_module_sig_body env me1.me_sig_body me2.me_sig_body &&
+    List.for_all2
+      (fun (_, mt1) (_, mt2) -> for_module_type env ~norm mt1 mt2)
+      me1.me_params me2.me_params &&
     let env, s = add_modules env me2.me_params me1.me_params in
     let comps1 = me1.me_comps in
     let comps2 = EcSubst.subst_module_comps s me2.me_comps in
diff --git a/src/ecThCloning.ml b/src/ecThCloning.ml
index 813556710..7d49e32e4 100644
--- a/src/ecThCloning.ml
+++ b/src/ecThCloning.ml
@@ -25,13 +25,14 @@ type ovkind =
 | OVK_Abbrev
 | OVK_Theory
 | OVK_Lemma
+| OVK_ModExpr
 | OVK_ModType
 
 type clone_error =
 | CE_UnkTheory         of qsymbol
 | CE_DupOverride       of ovkind * qsymbol
 | CE_UnkOverride       of ovkind * qsymbol
-| CE_ThyOverride       of qsymbol
+| CE_ThyOverride       of qsymbol * qsymbol
 | CE_UnkAbbrev         of qsymbol
 | CE_TypeArgMism       of ovkind * qsymbol
 | CE_OpIncompatible    of qsymbol * incompatible
@@ -39,6 +40,8 @@ type clone_error =
 | CE_TyIncompatible    of qsymbol * incompatible
 | CE_ModTyIncompatible of qsymbol
 | CE_ModIncompatible   of qsymbol
+| CE_ModStateful       of qsymbol * symbol list
+| CE_ModNotConcrete    of qsymbol
 | CE_InvalidRE         of string
 | CE_InlinedOpIsForm   of qsymbol
 | CE_ProofForLemma     of qsymbol
@@ -80,6 +83,7 @@ type evclone = {
   evc_ops      : (xop_override located) Msym.t;
   evc_preds    : (xpr_override located) Msym.t;
   evc_abbrevs  : (nt_override located) Msym.t;
+  evc_modexprs : (me_override located) Msym.t;
   evc_modtypes : (mt_override located) Msym.t;
   evc_lemmas   : evlemma;
   evc_ths      : (evclone * bool) Msym.t;
@@ -101,6 +105,7 @@ let evc_empty =
       evc_ops      = Msym.empty;
       evc_preds    = Msym.empty;
       evc_abbrevs  = Msym.empty;
+      evc_modexprs = Msym.empty;
       evc_modtypes = Msym.empty;
       evc_lemmas   = evl;
       evc_ths      = Msym.empty; }
@@ -407,6 +412,46 @@ end = struct
                pthp_tactic = Some tc; } in
     (pr :: proofs, evc)
 
+  (* ------------------------------------------------------------------ *)
+  (* Sound only for state-free modules: their own glob is empty, so AST-equal
+     components (checked at replay time) make source and target indiscernible. *)
+  let modexpr_ovrd oc ((proofs, evc) : state) name (med : me_override) =
+    let { pl_loc = lc; pl_desc = ((nm, x) as name) } = name in
+
+    let () =
+      match find_modexpr oc.oc_oth name with
+      | None ->
+         clone_error oc.oc_env (CE_UnkOverride (OVK_ModExpr, name))
+      | Some src ->
+         oiter
+           (fun path -> clone_error oc.oc_env (CE_ModStateful (name, path)))
+           (EcCoreModules.module_own_state src.tme_expr) in
+
+    let () =
+      let target = unloc (fst med) in
+
+      match EcEnv.Mod.lookup_opt target oc.oc_env with
+      | None ->
+         clone_error oc.oc_env (CE_UnkOverride (OVK_ModExpr, target))
+      | Some (mp, (dst, loca)) ->
+         match mp.EcPath.m_top, loca with
+         | `Concrete (_, None), Some _ ->
+            oiter
+              (fun path -> clone_error oc.oc_env (CE_ModStateful (target, path)))
+              (EcCoreModules.module_own_state dst)
+         | _ ->
+            clone_error oc.oc_env (CE_ModNotConcrete target) in
+
+    let evc =
+      evc_update
+        (fun evc ->
+         if Msym.mem x evc.evc_modexprs then
+           clone_error oc.oc_env (CE_DupOverride (OVK_ModExpr, name));
+         { evc with evc_modexprs = Msym.add x (mk_loc lc med) evc.evc_modexprs })
+        nm evc
+
+    in (proofs, evc)
+
   (* ------------------------------------------------------------------ *)
   let modtype_ovrd oc ((proofs, evc) : state) name (mtd : mt_override) =
     let { pl_loc = lc; pl_desc = ((nm, x) as name) } = name in
@@ -442,18 +487,23 @@ end = struct
       | Some ({cth_mode = `Concrete} as th) -> th
     in
 
-    (* FIXME improve error message *)
-    let rec contains_module cth =
-      let doit it =
-        match it.ti_item with
-        | Th_module _ -> true
-        | Th_theory (_, cth) -> contains_module cth
-        | _ -> false
-      in
-      List.exists doit cth.cth_items
-    in
-    if contains_module dth then
-      clone_error oc.oc_env (CE_ThyOverride name);
+    let stateful_module (cth : ctheory) : qsymbol option =
+      let rec doit prefix cth =
+        List.opick (fun it ->
+          match it.ti_item with
+          | Th_module me ->
+             omap
+               (fun _ -> (nm @ [x] @ prefix, me.tme_expr.me_name))
+               (EcCoreModules.module_own_state me.tme_expr)
+          | Th_theory (y, cth) ->
+             doit (prefix @ [y]) cth
+          | _ -> None)
+          cth.cth_items
+      in doit [] cth in
+
+    oiter
+      (fun mp -> clone_error oc.oc_env (CE_ThyOverride (name, mp)))
+      (stateful_module dth);
 
     let sp =
       match EcEnv.Theory.lookup_opt (unloc thd) oc.oc_env with
@@ -518,8 +568,10 @@ end = struct
       | Th_export _ ->
          (proofs, evc)
 
-      | Th_module _ ->
-         (proofs, evc)
+      | Th_module me ->
+        let x = me.tme_expr.me_name in
+        let ovrd = loced (EcPath.toqsymbol (tgpath ~kind:`Module x)) in
+        modexpr_ovrd oc (proofs, evc) (dtpath x) (ovrd, mode)
 
       | Th_modtype (x, _) ->
         let ovrd = loced (EcPath.toqsymbol (tgpath ~kind:`ModType x)) in
@@ -554,6 +606,9 @@ end = struct
      | PTHO_Axiom axd ->
         ax_ovrd oc state name axd
 
+     | PTHO_Module med ->
+       modexpr_ovrd oc state name med
+
      | PTHO_ModTyp mtd ->
        modtype_ovrd oc state name mtd
 
diff --git a/src/ecThCloning.mli b/src/ecThCloning.mli
index 4e7a8414a..31a453703 100644
--- a/src/ecThCloning.mli
+++ b/src/ecThCloning.mli
@@ -19,13 +19,14 @@ type ovkind =
 | OVK_Abbrev
 | OVK_Theory
 | OVK_Lemma
+| OVK_ModExpr
 | OVK_ModType
 
 type clone_error =
 | CE_UnkTheory         of qsymbol
 | CE_DupOverride       of ovkind * qsymbol
 | CE_UnkOverride       of ovkind * qsymbol
-| CE_ThyOverride       of qsymbol
+| CE_ThyOverride       of qsymbol * qsymbol
 | CE_UnkAbbrev         of qsymbol
 | CE_TypeArgMism       of ovkind * qsymbol
 | CE_OpIncompatible    of qsymbol * incompatible
@@ -33,6 +34,8 @@ type clone_error =
 | CE_TyIncompatible    of qsymbol * incompatible
 | CE_ModTyIncompatible of qsymbol
 | CE_ModIncompatible   of qsymbol
+| CE_ModStateful       of qsymbol * symbol list
+| CE_ModNotConcrete    of qsymbol
 | CE_InvalidRE         of string
 | CE_InlinedOpIsForm   of qsymbol
 | CE_ProofForLemma     of qsymbol
@@ -62,6 +65,7 @@ type evclone = {
   evc_ops      : (xop_override located) Msym.t;
   evc_preds    : (xpr_override located) Msym.t;
   evc_abbrevs  : (nt_override located) Msym.t;
+  evc_modexprs : (me_override located) Msym.t;
   evc_modtypes : (mt_override located) Msym.t;
   evc_lemmas   : evlemma;
   evc_ths      : (evclone * bool) Msym.t;
diff --git a/src/ecTheoryReplay.ml b/src/ecTheoryReplay.ml
index 380bc501d..72c264de9 100644
--- a/src/ecTheoryReplay.ml
+++ b/src/ecTheoryReplay.ml
@@ -973,12 +973,62 @@ and replay_modtype
 and replay_mod
   (ove : _ ovrenv) (subst, ops, proofs, scope) (import, (me : top_module_expr))
 =
+  match Msym.find_opt me.tme_expr.me_name ove.ovre_ovrd.evc_modexprs with
+  | None ->
     let subst, name = rename ove subst (`Module, me.tme_expr.me_name) in
     let me = EcSubst.subst_top_module subst me in
     let me = { me with tme_expr = { me.tme_expr with me_name = name } } in
     let item = (Th_module me) in
     (subst, ops, proofs, ove.ovre_hooks.hadd_item scope ~import item)
 
+  (* Both modules are state-free (enforced when the override is elaborated),
+     hence indiscernible once their components are found AST-equal below. *)
+  | Some { pl_desc = (target, mode) } ->
+    let name = me.tme_expr.me_name in
+    let env  = EcSection.env (ove.ovre_hooks.henv scope) in
+
+    assert (EcCoreModules.module_own_state me.tme_expr = None);
+
+    let mp, (newme, newlc) = EcEnv.Mod.lookup (unloc target) env in
+
+    let () =
+      match mp.EcPath.m_top with
+      | `Concrete (_, None) -> () | _ -> assert false in
+
+    let substme =
+      EcSubst.add_moddef subst
+        ~src:(EcPath.mpath_crt (xpath ove name) [] None) ~dst:mp in
+
+    let me    = EcSubst.subst_top_module substme me in
+    let me    = { me with tme_expr = { me.tme_expr with me_name = name } } in
+    let newme = { newme with me_name = name } in
+    let newme = { tme_expr = newme; tme_loca = Option.get newlc; } in
+
+    if not (EcReduction.EqTest.for_mexpr ~body:false env me.tme_expr newme.tme_expr) then
+      clone_error env (CE_ModIncompatible (snd ove.ovre_prefix, name));
+
+    let subst, name =
+      match mode with
+      | `Alias    -> rename ove subst (`Module, name)
+      | `Inline _ -> substme, name in
+
+    let scope =
+      if keep_of_mode mode then
+        let alias =
+          ME_Alias (
+            List.length newme.tme_expr.me_params,
+            EcPath.m_apply mp
+              (List.map
+                 (fun (id, _) -> EcPath.mident id)
+                 newme.tme_expr.me_params)) in
+        let newme =
+          { newme with tme_expr =
+              { newme.tme_expr with me_name = name; me_body = alias } } in
+        ove.ovre_hooks.hadd_item scope ~import (Th_module newme)
+      else scope in
+
+    (subst, ops, proofs, scope)
+
 (* -------------------------------------------------------------------- *)
 and replay_export
   (ove : _ ovrenv) (subst, ops, proofs, scope) (import, p, lc)
diff --git a/src/ecUserMessages.ml b/src/ecUserMessages.ml
index 763bec43a..eb2b5bf8e 100644
--- a/src/ecUserMessages.ml
+++ b/src/ecUserMessages.ml
@@ -825,6 +825,7 @@ end = struct
     | OVK_Abbrev    -> "abbreviation"
     | OVK_Theory    -> "theory"
     | OVK_Lemma     -> "lemma/axiom"
+    | OVK_ModExpr   -> "module"
     | OVK_ModType   -> "module type"
 
   let pp_incompatible env fmt = function
@@ -867,9 +868,9 @@ end = struct
         msg "unknown %s `%s'"
           (string_of_ovkind kd) (string_of_qsymbol x)
 
-    | CE_ThyOverride x ->
-        msg "Cannot override theory `%s`: contains module or exception"
-          (string_of_qsymbol x)
+    | CE_ThyOverride (x, m) ->
+        msg "Cannot override theory `%s': contains stateful module `%s'"
+          (string_of_qsymbol x) (string_of_qsymbol m)
 
     | CE_UnkAbbrev x ->
         msg "unknown abbreviation: `%s'" (string_of_qsymbol x)
@@ -898,6 +899,15 @@ end = struct
         msg "module `%s` is incompatible"
           (string_of_qsymbol x)
 
+    | CE_ModStateful (x, path) ->
+        let path = List.take (List.length path - 1) path in
+        msg "module `%s' declares state and cannot be overridden"
+          (String.concat "." (fst x @ [snd x] @ path))
+
+    | CE_ModNotConcrete x ->
+        msg "module `%s' is not a concrete top-level module"
+          (string_of_qsymbol x)
+
     | CE_InvalidRE x ->
         msg "invalid regexp: `%s'" x
 
diff --git a/tests/clone-module-stateless.ec b/tests/clone-module-stateless.ec
new file mode 100644
index 000000000..452404492
--- /dev/null
+++ b/tests/clone-module-stateless.ec
@@ -0,0 +1,574 @@
+(* Module overriding in clones is sound exactly for *stateless* modules: a
+   module that declares no program variable (transitively through its
+   sub-modules) has an empty own-glob, so once its components are AST-equal to
+   the target's it is indiscernible from it. Calling external stateful modules
+   and taking module parameters is fine; owning a variable never is. *)
+
+require import AllCore.
+
+(* ==================================================================== *)
+(*                              positive                                *)
+(* ==================================================================== *)
+
+(* -- P1: plain stateless module, the three override modes -------------- *)
+abstract theory P1.
+  module M = {
+    proc f (x : int) : int = { return x + 1; }
+  }.
+
+  lemma f_h (n : int) : hoare [M.f : x = n ==> res = n + 1].
+  proof. by proc; skip. qed.
+
+  lemma f_ph (n : int) : phoare [M.f : x = n ==> res = n + 1] = 1%r.
+  proof. by proc; skip. qed.
+end P1.
+
+module P1N = { proc f (x : int) : int = { return x + 1; } }.
+
+clone P1 as P1Clear with module M <- P1N.
+clone P1 as P1Keep  with module M <= P1N.
+clone P1 as P1Alias with module M  = P1N.
+
+lemma p1_clear (n : int) : hoare [P1N.f : x = n ==> res = n + 1].
+proof. by apply (P1Clear.f_h n). qed.
+
+lemma p1_keep (n : int) : phoare [P1Keep.M.f : x = n ==> res = n + 1] = 1%r.
+proof. by apply (P1Keep.f_ph n). qed.
+
+lemma p1_alias (n : int) : hoare [P1Alias.M.f : x = n ==> res = n + 1].
+proof. by apply (P1Alias.f_h n). qed.
+
+(* -- P2: stateless module writing an *external* stateful module -------- *)
+module S = { var x : int }.
+
+abstract theory P2.
+  module M = { proc f (n : int) : unit = { S.x <- n; } }.
+
+  lemma f_spec : hoare [M.f : n = 3 ==> S.x = 3].
+  proof. by proc; auto. qed.
+end P2.
+
+module P2N = { proc f (n : int) : unit = { S.x <- n; } }.
+
+clone P2 as P2C with module M <- P2N.
+
+lemma p2_use : hoare [P2N.f : n = 3 ==> S.x = 3].
+proof. by apply P2C.f_spec. qed.
+
+(* -- P3: stateless functor, lemma quantifying over a restricted adversary *)
+module type Adv = { proc a (x : int) : int }.
+
+abstract theory P3.
+  module G (A : Adv) = {
+    proc f (x : int) : int = { var r; r <@ A.a(x); return r; }
+  }.
+
+  lemma g_spec (A <: Adv{-S}) : hoare [G(A).f : S.x = 0 ==> true].
+  proof. by proc; call (: true). qed.
+end P3.
+
+module P3H (A : Adv) = {
+  proc f (x : int) : int = { var r; r <@ A.a(x); return r; }
+}.
+
+clone P3 as P3C with module G <- P3H.
+
+lemma p3_use (A <: Adv{-S}) : hoare [P3H(A).f : S.x = 0 ==> true].
+proof. by apply (P3C.g_spec A). qed.
+
+(* -- P3': the functor parameter may be alpha-renamed in the target ----- *)
+module P3H' (B : Adv) = {
+  proc f (x : int) : int = { var r; r <@ B.a(x); return r; }
+}.
+
+clone P3 as P3C' with module G <- P3H'.
+
+lemma p3'_use (A <: Adv{-S}) : hoare [P3H'(A).f : S.x = 0 ==> true].
+proof. by apply (P3C'.g_spec A). qed.
+
+(* -- P4: nested stateless sub-module ----------------------------------- *)
+abstract theory P4.
+  module M = {
+    module Sub = { proc g (x : int) : int = { return x + 1; } }
+
+    proc f (x : int) : int = { var r; r <@ Sub.g(x); return r; }
+  }.
+
+  lemma f_spec (n : int) : hoare [M.f : x = n ==> res = n + 1].
+  proof. by proc; inline *; auto. qed.
+end P4.
+
+module P4N = {
+  module Sub = { proc g (x : int) : int = { return x + 1; } }
+
+  proc f (x : int) : int = { var r; r <@ Sub.g(x); return r; }
+}.
+
+clone P4 as P4C with module M <- P4N.
+
+lemma p4_use (n : int) : hoare [P4N.f : x = n ==> res = n + 1].
+proof. by apply (P4C.f_spec n). qed.
+
+(* -- P5: theory override, the theory holding only stateless modules ---- *)
+theory P5Src.
+  module type I = { proc g (x : int) : int }.
+  module K = { proc f (x : int) : int = { return x + 1; } }.
+end P5Src.
+
+abstract theory P5.
+  theory Sub.
+    module type I = { proc g (x : int) : int }.
+    module K = { proc f (x : int) : int = { return x + 1; } }.
+  end Sub.
+
+  lemma k_spec (n : int) : hoare [Sub.K.f : x = n ==> res = n + 1].
+  proof. by proc; skip. qed.
+end P5.
+
+clone P5 as P5C with theory Sub <- P5Src.
+
+lemma p5_use (n : int) : hoare [P5Src.K.f : x = n ==> res = n + 1].
+proof. by apply (P5C.k_spec n). qed.
+
+(* -- P6: the target is itself a module alias (checked with ~body:false) - *)
+module P6Z = { proc f (x : int) : int = { return x + 1; } }.
+module P6Y = P6Z.
+
+abstract theory P6.
+  module M = { proc f (x : int) : int = { return x + 1; } }.
+
+  lemma f_spec (n : int) : hoare [M.f : x = n ==> res = n + 1].
+  proof. by proc; skip. qed.
+end P6.
+
+clone P6 as P6C with module M <- P6Y.
+
+lemma p6_use (n : int) : hoare [P6Y.f : x = n ==> res = n + 1].
+proof. by apply (P6C.f_spec n). qed.
+
+(* -- P6': the target is an alias of a functor application -------------- *)
+module type P6I = { proc a () : unit }.
+module P6A = { proc a () : unit = { } }.
+module P6F (X : P6I) = { proc f () : unit = { X.a(); } }.
+module P6R = P6F(P6A).
+
+abstract theory P6'.
+  module M = { proc f () : unit = { P6A.a(); } }.
+
+  lemma f_spec : hoare [M.f : true ==> true].
+  proof. by proc; inline *; auto. qed.
+end P6'.
+
+clone P6' as P6C' with module M <- P6R.
+
+lemma p6'_use : hoare [P6R.f : true ==> true].
+proof. by apply P6C'.f_spec. qed.
+
+(* -- P7: the module lives deep in a sub-theory path -------------------- *)
+abstract theory P7.
+  theory A. theory B.
+    module M = { proc f (x : int) : int = { return x + 1; } }.
+  end B. end A.
+
+  lemma f_spec (n : int) : hoare [A.B.M.f : x = n ==> res = n + 1].
+  proof. by proc; skip. qed.
+end P7.
+
+module P7N = { proc f (x : int) : int = { return x + 1; } }.
+
+clone P7 as P7C with module A.B.M <- P7N.
+
+lemma p7_use (n : int) : hoare [P7N.f : x = n ==> res = n + 1].
+proof. by apply (P7C.f_spec n). qed.
+
+(* -- P8: the module comes from an abstract sub-theory of the clonee ---- *)
+abstract theory P8Inner.
+  module M = { proc f (x : int) : int = { return x + 1; } }.
+
+  lemma f_spec (n : int) : hoare [M.f : x = n ==> res = n + 1].
+  proof. by proc; skip. qed.
+end P8Inner.
+
+abstract theory P8.
+  clone import P8Inner as I.
+end P8.
+
+module P8N = { proc f (x : int) : int = { return x + 1; } }.
+
+clone P8 as P8C with module I.M <- P8N.
+
+lemma p8_use (n : int) : hoare [P8N.f : x = n ==> res = n + 1].
+proof. by apply (P8C.I.f_spec n). qed.
+
+(* -- P9: an alias and a caller inside the clonee follow the override --- *)
+abstract theory P9.
+  module M = { proc f (x : int) : int = { return x + 1; } }.
+  module P = M.
+  module Q = { proc h (x : int) : int = { var r; r <@ M.f(x); return r; } }.
+
+  lemma p_spec (n : int) : hoare [P.f : x = n ==> res = n + 1].
+  proof. by proc; skip. qed.
+
+  lemma q_spec (n : int) : hoare [Q.h : x = n ==> res = n + 1].
+  proof. by proc; inline *; auto. qed.
+end P9.
+
+module P9N = { proc f (x : int) : int = { return x + 1; } }.
+
+clone P9 as P9C with module M <- P9N.
+
+lemma p9_use1 (n : int) : hoare [P9C.P.f : x = n ==> res = n + 1].
+proof. by apply (P9C.p_spec n). qed.
+
+lemma p9_use2 (n : int) : hoare [P9C.Q.h : x = n ==> res = n + 1].
+proof. by apply (P9C.q_spec n). qed.
+
+(* -- P10: the overridden module is itself an alias inside the clonee --- *)
+abstract theory P10.
+  module Base = { proc f (x : int) : int = { return x + 1; } }.
+  module M    = Base.
+
+  lemma f_spec (n : int) : hoare [M.f : x = n ==> res = n + 1].
+  proof. by proc; skip. qed.
+end P10.
+
+module P10N = { proc f (x : int) : int = { return x + 1; } }.
+
+clone P10 as P10C with module M <- P10N.
+
+lemma p10_use (n : int) : hoare [P10N.f : x = n ==> res = n + 1].
+proof. by apply (P10C.f_spec n). qed.
+
+(* -- P11: `glob` of a stateless module survives the override ----------- *)
+abstract theory P11.
+  module M = { proc f (x : int) : int = { return x + 1; } }.
+
+  lemma f_spec (g : glob M) (n : int) :
+    hoare [M.f : x = n /\ (glob M) = g ==> res = n + 1 /\ (glob M) = g].
+  proof. by proc; skip. qed.
+end P11.
+
+module P11N = { proc f (x : int) : int = { return x + 1; } }.
+
+clone P11 as P11C with module M <- P11N.
+
+lemma p11_use (g : glob P11N) (n : int) :
+  hoare [P11N.f : x = n /\ (glob P11N) = g ==> res = n + 1 /\ (glob P11N) = g].
+proof. by apply (P11C.f_spec g n). qed.
+
+(* -- P12: two stateless modules may be identified with the same target - *)
+abstract theory P12.
+  module M1 = { proc f (x : int) : int = { return x + 1; } }.
+  module M2 = { proc f (x : int) : int = { return x + 1; } }.
+
+  lemma eq_spec : equiv [M1.f ~ M2.f : ={x} ==> ={res}].
+  proof. by proc; skip. qed.
+end P12.
+
+module P12N = { proc f (x : int) : int = { return x + 1; } }.
+
+clone P12 as P12C with module M1 <- P12N, module M2 <- P12N.
+
+lemma p12_use : equiv [P12N.f ~ P12N.f : ={x} ==> ={res}].
+proof. by apply P12C.eq_spec. qed.
+
+(* -- P13: a module override combines with `rename` and a modtype override *)
+module type P13I = { proc a () : unit }.
+
+abstract theory P13.
+  module type J = { proc a () : unit }.
+  module M = { proc f (x : int) : int = { return x + 1; } }.
+
+  lemma foo (n : int) : hoare [M.f : x = n ==> res = n + 1].
+  proof. by proc; skip. qed.
+end P13.
+
+module P13N = { proc f (x : int) : int = { return x + 1; } }.
+
+clone P13 as P13C with
+  module type J <- P13I,
+  module M       = P13N
+  rename [module] "M" as "MM" "foo" as "bar".
+
+lemma p13_use (n : int) : hoare [P13C.MM.f : x = n ==> res = n + 1].
+proof. by apply (P13C.bar n). qed.
+
+(* -- P14: a module kept by `clone include ... <=` stays overridable ---- *)
+module P14N = { proc f (x : int) : int = { return x + 1; } }.
+module P14P = { proc f (x : int) : int = { return x + 1; } }.
+
+theory P14Mid.
+  clone include P1 with module M <= P14N.
+end P14Mid.
+
+lemma p14_use (n : int) : hoare [P14N.f : x = n ==> res = n + 1].
+proof. by apply (P14Mid.f_h n). qed.
+
+clone P14Mid as P14C with module M <- P14P.
+
+(* -- P15: theory override carrying a stateless functor ----------------- *)
+theory P15Src.
+  module G (A : Adv) = {
+    proc f (x : int) : int = { var r; r <@ A.a(x); return r; }
+  }.
+end P15Src.
+
+abstract theory P15.
+  theory Sub.
+    module G (A : Adv) = {
+      proc f (x : int) : int = { var r; r <@ A.a(x); return r; }
+    }.
+  end Sub.
+
+  lemma g_spec (A <: Adv) : hoare [Sub.G(A).f : true ==> true].
+  proof. by proc; call (: true). qed.
+end P15.
+
+clone P15 as P15C with theory Sub <- P15Src.
+
+lemma p15_use (A <: Adv) : hoare [P15Src.G(A).f : true ==> true].
+proof. by apply (P15C.g_spec A). qed.
+
+(* ==================================================================== *)
+(*                              negative                                *)
+(* ==================================================================== *)
+
+(* -- N1: the #380 unsoundness (oskgo's `module A2.M <- A1.M`) ---------- *)
+abstract theory N1A.
+  module M = {
+    var x : int
+
+    proc f () : unit = { x <- 1; }
+  }.
+end N1A.
+
+theory N1B.
+  clone N1A as A1.
+  clone N1A as A2.
+
+  (* A1.M and A2.M own *distinct* variables; identifying them proves False. *)
+  lemma sep : hoare [A1.M.f : A2.M.x = 0 ==> A2.M.x = 0].
+  proof. by proc; auto. qed.
+end N1B.
+
+expect fail "module `A2.M' declares state and cannot be overridden"
+clone N1B as N1B1 with module A2.M <- A1.M.
+
+(* -- N1': the same unsoundness through Unruh's `theory A2 <- A1` ------- *)
+expect fail "Cannot override theory `A2': contains stateful module `A2.M'"
+clone N1B as N1B2 with theory A2 <- A1.
+
+(* -- N2: stateless source, stateful target ----------------------------- *)
+abstract theory N2.
+  module M = { proc f () : unit = { } }.
+end N2.
+
+module N2N = { var x : int  proc f () : unit = { } }.
+
+expect fail "module `N2N' declares state and cannot be overridden"
+clone N2 as N2C with module M <- N2N.
+
+(* -- N3: state hidden in a nested sub-module --------------------------- *)
+abstract theory N3.
+  module M = {
+    module Sub = { var x : int  proc g () : unit = { } }
+
+    proc f () : unit = { Sub.g(); }
+  }.
+end N3.
+
+module N3N = {
+  module Sub = { var x : int  proc g () : unit = { } }
+
+  proc f () : unit = { Sub.g(); }
+}.
+
+expect fail "module `M.Sub' declares state and cannot be overridden"
+clone N3 as N3C with module M <- N3N.
+
+(* -- N3': state three sub-modules deep --------------------------------- *)
+abstract theory N3'.
+  module M = {
+    module A = { module B = { var x : int  proc g () : unit = { } } }
+
+    proc f () : unit = { }
+  }.
+end N3'.
+
+module N3'N = {
+  module A = { module B = { var x : int  proc g () : unit = { } } }
+
+  proc f () : unit = { }
+}.
+
+expect fail "module `M.A.B' declares state and cannot be overridden"
+clone N3' as N3'C with module M <- N3'N.
+
+(* -- N3'': state reached through a sub-module aliasing a stateful module  *)
+module N3''S = { var x : int  proc g () : unit = { x <- 1; } }.
+
+abstract theory N3''.
+  module M = { module Sub = N3''S  proc f () : unit = { Sub.g(); } }.
+end N3''.
+
+module N3''N = { module Sub = N3''S  proc f () : unit = { Sub.g(); } }.
+
+expect fail "module `M.Sub' declares state and cannot be overridden"
+clone N3'' as N3''C with module M <- N3''N.
+
+(* -- N3''': state behind a restricting signature is still state -------- *)
+abstract theory N3'''.
+  module M : P13I = { var x : int  proc a () : unit = { x <- 1; } }.
+end N3'''.
+
+module N3'''N : P13I = { var x : int  proc a () : unit = { x <- 1; } }.
+
+expect fail "module `M' declares state and cannot be overridden"
+clone N3''' as N3'''C with module M <- N3'''N.
+
+(* -- N3'''': a top-level alias of a stateful module is stateful -------- *)
+module N3AliasS = { var x : int  proc f () : unit = { x <- 1; } }.
+module N3AliasY = N3AliasS.
+
+abstract theory N3Alias.
+  module M = { proc f () : unit = { } }.
+end N3Alias.
+
+expect fail "module `N3AliasY' declares state and cannot be overridden"
+clone N3Alias as N3AliasC with module M <- N3AliasY.
+
+(* -- N4: same signature, different body -------------------------------- *)
+abstract theory N4.
+  module M = { proc f (x : int) : int = { return x + 1; } }.
+end N4.
+
+module N4N = { proc f (x : int) : int = { return x + 2; } }.
+
+expect fail "module `M` is incompatible"
+clone N4 as N4C with module M <- N4N.
+
+(* -- N4': same names, different number of procedures ------------------- *)
+abstract theory N4'.
+  module M = { proc f () : unit = { }  proc g () : unit = { } }.
+end N4'.
+
+module N4'N = { proc f () : unit = { } }.
+
+expect fail "module `M` is incompatible"
+clone N4' as N4'C with module M <- N4'N.
+
+(* -- N4'': parameter arity mismatch (non-functor vs functor) ----------- *)
+abstract theory N4''.
+  module M = { proc f () : unit = { } }.
+end N4''.
+
+module N4''N (A : Adv) = { proc f () : unit = { } }.
+
+expect fail "module `M` is incompatible"
+clone N4'' as N4''C with module M <- N4''N.
+
+(* -- N4''': same arity, different parameter module type ---------------- *)
+module type N4'''J = { proc b () : unit }.
+
+abstract theory N4'''.
+  module M (A : Adv) = { proc f () : unit = { } }.
+  lemma foo (A <: Adv) : hoare [M(A).f : true ==> true] by proc.
+end N4'''.
+
+module N4'''N (A : N4'''J) = { proc f () : unit = { } }.
+
+expect fail "module `M` is incompatible"
+clone N4''' as N4'''C with module M <- N4'''N.
+
+expect fail "module `M` is incompatible"
+clone N4''' as N4'''D with module M <- N4'N.
+
+(* -- N5: the target is a `declare module` ------------------------------ *)
+abstract theory N5.
+  module M = { proc a () : unit = { } }.
+end N5.
+
+section.
+declare module N5D <: P13I.
+
+expect fail "module `N5D' is not a concrete top-level module"
+clone N5 as N5C with module M <- N5D.
+
+end section.
+
+(* -- N6: theory override with a stateful module inside ----------------- *)
+theory N6Src.
+  module K = { var y : int  proc f () : unit = { } }.
+end N6Src.
+
+abstract theory N6.
+  theory Sub.
+    module K = { var y : int  proc f () : unit = { } }.
+  end Sub.
+end N6.
+
+expect fail "Cannot override theory `Sub': contains stateful module `Sub.K'"
+clone N6 as N6C with theory Sub <- N6Src.
+
+(* -- N6': theory override whose *target* module is the stateful one ---- *)
+theory N6'Src.
+  module K = { var y : int  proc f () : unit = { } }.
+end N6'Src.
+
+abstract theory N6'.
+  theory Sub.
+    module K = { proc f () : unit = { } }.
+  end Sub.
+end N6'.
+
+expect fail "module `Top.N6'Src.K' declares state and cannot be overridden"
+clone N6' as N6'C with theory Sub <- N6'Src.
+
+(* -- N7: the same module overridden twice ------------------------------ *)
+abstract theory N7.
+  module M = { proc f () : unit = { } }.
+end N7.
+
+module N7N = { proc f () : unit = { } }.
+module N7P = { proc f () : unit = { } }.
+
+expect fail "the module `M' is instantiate twice"
+clone N7 as N7C with module M <- N7N, module M <- N7P.
+
+(* -- N8: unknown source, unknown target -------------------------------- *)
+abstract theory N8.
+  module M = { proc f () : unit = { } }.
+end N8.
+
+module N8N = { proc f () : unit = { } }.
+
+expect fail "unknown module `NoSuchModule'"
+clone N8 as N8C1 with module NoSuchModule <- N8N.
+
+expect fail "unknown module `NoSuchModule'"
+clone N8 as N8C2 with module M <- NoSuchModule.
+
+(* -- N9: a module cleared by `<-` is gone from the clone --------------- *)
+clone N8 as N9C with module M <- N8N.
+
+expect fail "unknown module `M'"
+clone N9C as N9D with module M <- N8N.
+
+(* -- N10: a functor owning a variable is stateful ---------------------- *)
+abstract theory N10.
+  module G (A : Adv) = { var x : int  proc f () : unit = { x <- 1; } }.
+end N10.
+
+module N10H (A : Adv) = { var x : int  proc f () : unit = { x <- 1; } }.
+
+expect fail "module `G' declares state and cannot be overridden"
+clone N10 as N10C with module G <- N10H.
+
+(* -- N11: a section-local target may not leak into a global lemma ------ *)
+section.
+local module N11N = { proc f (x : int) : int = { return x + 1; } }.
+
+expect fail "lemma/axiom f_h cannot depend on local module N11N"
+clone P1 as N11C with module M <- N11N.
+
+end section.