Fix for bug #21527.

When cloning a module using another module with a nullary symbol with some
regions, these regions were no longer available to clone the declarations
that were using them.

src/whyml/mlw_decl.ml

@@ -161,7 +161,12 @@ let check_vars vars =
       (Stv.choose vars.vars_tv).tv_name.id_string
 
 let letvar_news = function
-  | LetV pv -> check_vars pv.pv_ity.ity_vars; Sid.singleton pv.pv_vs.vs_name
+  | LetV pv ->
+    check_vars pv.pv_ity.ity_vars;
+    Sreg.fold
+      (fun r acc -> Sid.add r.reg_name acc)
+      pv.pv_ity.ity_vars.vars_reg
+      (Sid.singleton pv.pv_vs.vs_name)
   | LetA ps -> check_vars ps.ps_vars; Sid.singleton ps.ps_name
 
 let ids_of_pvset s pvs =

src/whyml/mlw_module.ml

@@ -615,7 +615,8 @@ let clone_export uc m minst inst =
           let id = id_clone ps.ps_name in
           let aty = conv_aty !mvs ps.ps_aty in
           let vari = Spv.fold (fun pv l ->
-            (t_var (Mvs.find pv.pv_vs !mvs), None)::l) ps.ps_pvset [] in
+            (t_var (Mvs.find_def pv.pv_vs pv.pv_vs !mvs), None)::l)
+            ps.ps_pvset [] in
           (* we save all external pvsymbols to preserve the effects *)
           let spec = { aty.aty_spec with c_variant = vari } in
           let aty = vty_arrow ~spec aty.aty_args aty.aty_result in