diff --git a/compiler/Makefile b/compiler/Makefile
index 47a167f41c..5bca556f86 100644
--- a/compiler/Makefile
+++ b/compiler/Makefile
@@ -39,10 +39,10 @@ all:
 	for p in _build/install/default/bin/*; do ln -sf $$p $$(basename $$p); done
 
 CIL:
-	$(RM) -f src/CIL/*.ml src/CIL/*.mli ../proofs/extraction.vo
+	$(RM) -f src/CIL/*.ml src/CIL/*.mli
 	$(MAKE) -C ../proofs extraction
-	cp ../proofs/lang/ocaml/*.ml  src/CIL/
-	cp ../proofs/lang/ocaml/*.mli src/CIL/
+	cp ../proofs/_build/default/extraction/*.ml  src/CIL/
+	cp ../proofs/_build/default/extraction/*.mli src/CIL/
 
 check: all
 	$(CHECK) --report=report.log $(CHECKCATS)
diff --git a/compiler/entry/commonCLI.ml b/compiler/entry/commonCLI.ml
index 65533c9bad..86bbc36ac0 100644
--- a/compiler/entry/commonCLI.ml
+++ b/compiler/entry/commonCLI.ml
@@ -91,8 +91,8 @@ let parse_and_compile (type reg regx xreg rflag cond asm_op extra_op)
       let cp = Conv.cuprog_of_prog prog in
       (* We need to avoid catching compilation errors. *)
       match Compile.compile (module Arch) stop prog cp with
-      | Utils0.Ok _ -> assert false
-      | Utils0.Error e ->
+      | Result.Ok _ -> assert false
+      | Result.Error e ->
           let e = Conv.error_of_cerror (Printer.pp_err ~debug:false) e in
           raise (HiError e)
       | exception Found -> !res
diff --git a/compiler/src/compile.ml b/compiler/src/compile.ml
index 0e1d80fab5..362f29d574 100644
--- a/compiler/src/compile.ml
+++ b/compiler/src/compile.ml
@@ -63,8 +63,8 @@ let do_spill_unspill asmop ?(debug = false) cp =
       (fun k ii -> Conv.fresh_var_ident k ii (Uint63.of_int 0))
       p
   with
-  | Utils0.Error msg -> Error (Conv.error_of_cerror (Printer.pp_err ~debug) msg)
-  | Utils0.Ok p -> Ok (Conv.prog_of_cuprog p)
+  | Result.Error msg -> Error (Conv.error_of_cerror (Printer.pp_err ~debug) msg)
+  | Result.Ok p -> Ok (Conv.prog_of_cuprog p)
 
 let do_wint_int
    (type reg regx xreg rflag cond asm_op extra_op)
@@ -98,8 +98,8 @@ let do_wint_int
   let cp = Wint_int.wi2i_prog Arch.asmOp Arch.msf_size info cp in
   let cp =
     match cp with
-    | Utils0.Ok cp -> cp
-    | Utils0.Error e ->
+    | Result.Ok cp -> cp
+    | Result.Error e ->
       let e = Conv.error_of_cerror (Printer.pp_err ~debug:false) e in
       raise (HiError e) in
   let (gd, fdso) = Conv.prog_of_cuprog cp in
diff --git a/compiler/src/conv.ml b/compiler/src/conv.ml
index 25cd39d0aa..feba33cf88 100644
--- a/compiler/src/conv.ml
+++ b/compiler/src/conv.ml
@@ -292,7 +292,7 @@ let to_array ty p t =
   let ws, n = array_kind ty in
   let get i = 
     match Warray_.WArray.get p Aligned Warray_.AAscale ws t (cz_of_int i) with
-    | Utils0.Ok w -> z_of_word ws w
+    | Result.Ok w -> z_of_word ws w
     | _    -> assert false in
   ws, Array.init n get
 
diff --git a/compiler/src/evaluator.ml b/compiler/src/evaluator.ml
index 62944929e3..a930360389 100644
--- a/compiler/src/evaluator.ml
+++ b/compiler/src/evaluator.ml
@@ -1,5 +1,6 @@
 open BinNums
-open Utils0 
+open Utils0
+open Result
 open Type
 open Sem_type
 open Warray_
@@ -11,7 +12,7 @@ open Psem_defs
 open Values
 open Sem_params
          
-exception Eval_error of instr_info * Utils0.error 
+exception Eval_error of instr_info * error
 
 let pp_error fmt err =
   Format.fprintf fmt "%s" @@
diff --git a/compiler/src/evaluator.mli b/compiler/src/evaluator.mli
index 20c7017c65..74c7aa838a 100644
--- a/compiler/src/evaluator.mli
+++ b/compiler/src/evaluator.mli
@@ -1,4 +1,4 @@
-exception Eval_error of Expr.instr_info * Utils0.error
+exception Eval_error of Expr.instr_info * Result.error
 
 val exec :
   'syscall_state Sem_params.coq_EstateParams ->
@@ -33,4 +33,4 @@ val run :
   Low_memory.Memory.mem * Values.values
 
 val pp_val : Format.formatter -> Values.value -> unit
-val pp_error : Format.formatter -> Utils0.error -> unit
+val pp_error : Format.formatter -> Result.error -> unit
diff --git a/compiler/src/main_compiler.ml b/compiler/src/main_compiler.ml
index 152870d386..0d48892608 100644
--- a/compiler/src/main_compiler.ml
+++ b/compiler/src/main_compiler.ml
@@ -212,8 +212,8 @@ let main () =
               (match
                  Evaluator.initial_memory Arch.reg_size (Z.of_string "1024") m
                with
-               | Utils0.Ok m -> m
-               | Utils0.Error err -> raise (Evaluator.Eval_error (ii, err)))
+               | Result.Ok m -> m
+               | Result.Error err -> raise (Evaluator.Eval_error (ii, err)))
               |> Evaluator.run
                    (module Arch)
                    (Expr.to_uprog Arch.asmOp cprog)
@@ -231,10 +231,10 @@ let main () =
       end;
 
     begin match Compile.compile (module Arch) visit_prog_after_pass prog cprog with
-    | Utils0.Error e ->
+    | Result.Error e ->
       let e = Conv.error_of_cerror (Printer.pp_err ~debug:!debug) e in
       raise (HiError e)
-    | Utils0.Ok asm ->
+    | Result.Ok asm ->
       if !outfile <> "" then begin
         BatFile.with_file_out !outfile (fun out ->
           let fmt = BatFormat.formatter_of_out_channel out in
diff --git a/compiler/src/stackAlloc.ml b/compiler/src/stackAlloc.ml
index 9d42f6d962..a48765b02f 100644
--- a/compiler/src/stackAlloc.ml
+++ b/compiler/src/stackAlloc.ml
@@ -194,16 +194,16 @@ let memory_analysis pp_sr pp_err ~debug up =
         get_sao
         up
     with
-    | Utils0.Ok sp -> sp
-    | Utils0.Error e ->
+    | Result.Ok sp -> sp
+    | Result.Error e ->
       let e = Conv.error_of_cerror pp_err e in
       raise (HiError e)
   in
 
   let sp' =
     match Arch.aparams.ap_lap (Conv.fresh_var_ident (Reg (Normal, Direct)) IInfo.dummy (Uint63.of_int 0)) sp with
-    | Utils0.Ok sp -> sp
-    | Utils0.Error e ->
+    | Result.Ok sp -> sp
+    | Result.Error e ->
       let e = Conv.error_of_cerror pp_err e in
       raise (HiError e)
   in
@@ -235,8 +235,8 @@ let memory_analysis pp_sr pp_err ~debug up =
     let (fn, cfd) = Conv.cufdef_of_fdef fd in
     let fd = 
       match Dead_code.dead_code_fd Arch.asmOp Arch.aparams.ap_is_move_op false tokeep fn cfd with
-      | Utils0.Ok cfd -> Conv.fdef_of_cufdef (fn, cfd)
-      | Utils0.Error _ -> assert false in 
+      | Result.Ok cfd -> Conv.fdef_of_cufdef (fn, cfd)
+      | Result.Error _ -> assert false in 
     (extra,fd) in
   let fds = List.map deadcode fds in
   if debug then
diff --git a/compiler/src/x86_arch_full.ml b/compiler/src/x86_arch_full.ml
index 292cb4fc97..fb5c86c02a 100644
--- a/compiler/src/x86_arch_full.ml
+++ b/compiler/src/x86_arch_full.ml
@@ -15,10 +15,13 @@ let atoI decl =
     V.mk s (Reg(k,Direct)) (Conv.ty_of_cty t) L._dummy [] in
 
   match Arch_extra.MkAToIdent.mk decl mk_var with
-  | Utils0.Error e ->
+  | Result.Error e ->
+      (* FIXME: in this experiment, Arch_extra.MkAToIdent.mk returns a string
+         in the error case, so it is not clear what to do here *)
+      assert false (*
       let e = Conv.error_of_cerror (Printer.pp_err ~debug:true) e in
-      raise (Utils.HiError e)
-  | Utils0.Ok atoI -> atoI
+      raise (Utils.HiError e) *)
+  | Result.Ok atoI -> atoI
 
 module X86_core = struct
   type reg = register
diff --git a/compiler/tests/exec/execlib.ml b/compiler/tests/exec/execlib.ml
index 64f82bdcb5..3e189a6396 100644
--- a/compiler/tests/exec/execlib.ml
+++ b/compiler/tests/exec/execlib.ml
@@ -27,8 +27,8 @@ let load_file name =
 
 let init_memory ms =
   match Evaluator.initial_memory Arch.reg_size (Z.of_int 1024) ms with
-  | Utils0.Error _err -> assert false
-  | Utils0.Ok m -> m
+  | Result.Error _err -> assert false
+  | Result.Ok m -> m
 
 let exec (fs, prog) ms f args =
   let f = Hashtbl.find fs f in
diff --git a/proofs/Makefile b/proofs/Makefile
index ebfba70dfb..a446fcfa11 100644
--- a/proofs/Makefile
+++ b/proofs/Makefile
@@ -15,9 +15,7 @@ uninstall: Makefile.coq
 	$(MAKE) -f Makefile.coq uninstall
 
 extraction: Makefile.coq
-	$(RM) lang/ocaml/*.ml lang/ocaml/*.mli
-	$(RM) lang/extraction.vo
-	+$(COQMAKE) lang/extraction.vo
+	dune build extraction
 
 # --------------------------------------------------------------------
 this-clean::
diff --git a/proofs/_CoqProject b/proofs/_CoqProject
index b6ccac5303..a0376079db 100644
--- a/proofs/_CoqProject
+++ b/proofs/_CoqProject
@@ -21,8 +21,6 @@
 -R ssrmisc Jasmin
 -R itrees Jasmin
 
-ssrmisc/oseq.v
-ssrmisc/seq_extra.v
 3rdparty/ssrring.v
 3rdparty/xseq.v
 arch/arch_decl.v
@@ -38,6 +36,7 @@ compiler/allocation.v
 compiler/allocation_proof.v
 compiler/arch_params.v
 compiler/arch_params_proof.v
+compiler/arm.v
 compiler/arm_decl.v
 compiler/arm_extra.v
 compiler/arm_facts.v
@@ -46,23 +45,22 @@ compiler/arm_instr_decl_lemmas.v
 compiler/arm_lowering.v
 compiler/arm_lowering_proof.v
 compiler/arm_params.v
-compiler/arm_params_proof.v
 compiler/arm_params_common.v
 compiler/arm_params_common_proof.v
 compiler/arm_params_core.v
 compiler/arm_params_core_proof.v
+compiler/arm_params_proof.v
 compiler/arm_stack_zeroization.v
 compiler/arm_stack_zeroization_proof.v
-compiler/arm.v
-compiler/array_expansion.v
-compiler/array_expansion_proof.v
 compiler/array_copy.v
 compiler/array_copy_proof.v
+compiler/array_expansion.v
+compiler/array_expansion_proof.v
 compiler/array_init.v
 compiler/array_init_proof.v
-compiler/compiler_util.v
 compiler/compiler.v
 compiler/compiler_proof.v
+compiler/compiler_util.v
 compiler/constant_prop.v
 compiler/constant_prop_proof.v
 compiler/dead_calls.v
@@ -80,9 +78,10 @@ compiler/linearization.v
 compiler/linearization_proof.v
 compiler/load_constants_in_cond.v
 compiler/load_constants_in_cond_proof.v
-compiler/lowering.v
 compiler/lower_spill.v
 compiler/lower_spill_proof.v
+compiler/lowering.v
+compiler/lowering_lemmas.v
 compiler/makeReferenceArguments.v
 compiler/makeReferenceArguments_proof.v
 compiler/merge_varmaps.v
@@ -90,24 +89,24 @@ compiler/merge_varmaps_proof.v
 compiler/post_unrolling_check.v
 compiler/propagate_inline.v
 compiler/propagate_inline_proof.v
+compiler/remove_globals.v
+compiler/remove_globals_proof.v
 compiler/riscv.v
 compiler/riscv_decl.v
-compiler/riscv_instr_decl.v
 compiler/riscv_extra.v
+compiler/riscv_instr_decl.v
 compiler/riscv_lower_addressing.v
 compiler/riscv_lower_addressing_proof.v
 compiler/riscv_lowering.v
 compiler/riscv_lowering_proof.v
 compiler/riscv_params.v
-compiler/riscv_params_proof.v
-compiler/riscv_params_core.v
-compiler/riscv_params_core_proof.v
 compiler/riscv_params_common.v
 compiler/riscv_params_common_proof.v
+compiler/riscv_params_core.v
+compiler/riscv_params_core_proof.v
+compiler/riscv_params_proof.v
 compiler/riscv_stack_zeroization.v
 compiler/riscv_stack_zeroization_proof.v
-compiler/remove_globals.v
-compiler/remove_globals_proof.v
 compiler/slh_lowering.v
 compiler/slh_lowering_proof.v
 compiler/stack_alloc.v
@@ -127,6 +126,7 @@ compiler/wint_int.v
 compiler/wint_int_proof.v
 compiler/wint_word.v
 compiler/wint_word_proof.v
+compiler/x86.v
 compiler/x86_decl.v
 compiler/x86_extra.v
 compiler/x86_instr_decl.v
@@ -136,7 +136,6 @@ compiler/x86_params.v
 compiler/x86_params_proof.v
 compiler/x86_stack_zeroization.v
 compiler/x86_stack_zeroization_proof.v
-compiler/x86.v
 itrees/it_exec.v
 itrees/rutt_extras.v
 itrees/xrutt.v
@@ -159,26 +158,25 @@ lang/linear.v
 lang/linear_facts.v
 lang/linear_sem.v
 lang/low_memory.v
-lang/lowering_lemmas.v
 lang/memory_example.v
 lang/memory_model.v
 lang/one_varmap.v
 lang/psem.v
-lang/psem_defs.v
 lang/psem_core.v
+lang/psem_defs.v
+lang/psem_facts.v
 lang/psem_of_sem_proof.v
 lang/pseudo_operator.v
-lang/psem_facts.v
 lang/relational_logic.v
 lang/sem_one_varmap.v
-lang/sem_op_typed.v
 lang/sem_one_varmap_facts.v
+lang/sem_op_typed.v
 lang/sem_params.v
 lang/sem_type.v
 lang/sha256.v
 lang/shift_kind.v
-lang/sopn.v
 lang/slh_ops.v
+lang/sopn.v
 lang/stack_zero_strategy.v
 lang/strings.v
 lang/syscall.v
@@ -193,3 +191,5 @@ lang/waes.v
 lang/warray_.v
 lang/word.v
 lang/wsize.v
+ssrmisc/oseq.v
+ssrmisc/seq_extra.v
diff --git a/proofs/arch/_CoqProject b/proofs/arch/_CoqProject
new file mode 100644
index 0000000000..c06c783e05
--- /dev/null
+++ b/proofs/arch/_CoqProject
@@ -0,0 +1,23 @@
+-R ../_build/default/common common
+-R ../_build/default/itrees itrees
+-R ../_build/default/lang lang
+-R ../_build/default/ssrmisc ssrmisc
+-R ../_build/default/thirdparty thirdparty
+
+-R ../_build/default/arch arch
+
+-arg "-set" -arg "'Uniform Inductive Parameters'"
+-arg "-set" -arg "'Implicit Arguments'"
+-arg "-unset" -arg "'Strict Implicit'"
+-arg "-unset" -arg "'Printing Implicit Defensive'"
+-arg "-w -notation-overridden"
+-arg "-w -extraction-reserved-identifier"
+-arg "-w -extraction-opaque-accessed"
+-arg "-w -ambiguous-paths"
+-arg "-w -redundant-canonical-projection"
+-arg "-w -projection-no-head-constant"
+-arg "-w -postfix-notation-not-level-1"
+-arg "-w -deprecated-since-mathcomp-2.3.0"
+-arg "-w -deprecated-since-mathcomp-2.4.0"
+-arg "-w -deprecated-from-Coq"
+-arg "-w -deprecated-dirpath-Coq"
diff --git a/proofs/arch/arch_decl.v b/proofs/arch/arch_decl.v
index 72ce279298..19a1c43bd9 100644
--- a/proofs/arch/arch_decl.v
+++ b/proofs/arch/arch_decl.v
@@ -7,11 +7,11 @@ From Coq Require Import
   Relation_Operators
   Utf8.
 
-Require Import
+From ssrmisc Require Import oseq.
+From lang Require Import
   global
   label
   memory_model
-  oseq
   sem_type
   strings
   syscall
@@ -19,11 +19,11 @@ Require Import
   expr
   word.
 
-Require Import
+From lang Require Import
   sopn
   flag_combination
-  shift_kind
-  arm_expand_imm.
+  shift_kind.
+Require Import arm_expand_imm.
 
 (* -------------------------------------------------------------------- *)
 (* String representation of architecture components.
diff --git a/proofs/arch/arch_extra.v b/proofs/arch/arch_extra.v
index 3502fd51bd..d338a9e165 100644
--- a/proofs/arch/arch_extra.v
+++ b/proofs/arch/arch_extra.v
@@ -1,8 +1,9 @@
 (* -------------------------------------------------------------------- *)
 From HB Require Import structures.
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype.
-Require Import xseq strings utils var type values sopn expr fexpr arch_decl.
-Require Import compiler_util.
+From thirdparty Require Import xseq.
+From lang Require Import strings utils var type values sopn expr fexpr.
+Require Import arch_decl.
 
 Section ToIdent.
 
@@ -68,7 +69,7 @@ Arguments to_var {t} {T}%_type_scope {tS toI} r.
 Module Type MkToIdent_T.
 
   Parameter mk : forall (t:stype) (T:Type) {tS: ToString t T},
-    (string -> Ident.ident) -> result pp_error_loc (ToIdent T).
+    (string -> Ident.ident) -> result string (ToIdent T).
 
 End MkToIdent_T.
 
@@ -138,7 +139,7 @@ Module MkToIdent : MkToIdent_T.
         ok {| inj_to_ident := to_identI is_uniq
             ; of_identE := of_IdentE
             |}
-    | _ => Error (pp_internal_error_s "to_ident generation" category)
+    | _ => Error ("to_ident generation of " ++ category)%string
     end.
 
   End Section.
@@ -166,7 +167,7 @@ Module Type AToIdent_T.
 
   Parameter mk :
     forall `{arch : arch_decl},
-      (reg_kind -> stype -> string -> Ident.ident) ->  result pp_error_loc arch_toIdent.
+      (reg_kind -> stype -> string -> Ident.ident) -> result string arch_toIdent.
 
 End AToIdent_T.
 
@@ -208,7 +209,7 @@ Module MkAToIdent : AToIdent_T.
             ; toI_f  := toI_f
             ; inj_toI_reg_regx := inj_toI_reg_regxP h
            |}
-    | _ => Error (pp_internal_error_s "arch_to_ident generation" "inj_toI_reg_regx")
+    | _ => Error ("arch_to_ident generation in inj_toI_reg_regx")%string
     end.
 
   End Section.
@@ -266,7 +267,7 @@ Class asm_extra (reg regx xreg rflag cond asm_op extra_op : Type) :=
     -> extra_op
     -> lexprs
     -> rexprs
-    -> cexec (seq (asm_op_msb_t * lexprs * rexprs))
+    -> result (bool * string) (seq (asm_op_msb_t * lexprs * rexprs))
   }.
 
 #[global]
diff --git a/proofs/arch/arch_sem.v b/proofs/arch/arch_sem.v
index b69dbd7a1f..7ce121d9df 100644
--- a/proofs/arch/arch_sem.v
+++ b/proofs/arch/arch_sem.v
@@ -1,21 +1,20 @@
 From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat eqtype finfun.
 From mathcomp Require Import ssralg word_ssrZ.
-Require oseq.
 From Coq Require Import
   ZArith
   Utf8
   Relation_Operators.
-Require Import
+From lang Require Import
   utils
   strings
   memory_model
   (* word *)
   global
-  oseq
   sem_type
   syscall syscall_sem
-  label
-  arch_decl.
+  label.
+From ssrmisc Require Import oseq.
+Require Import arch_decl.
 
 (* -------------------------------------------------------------------- *)
 
diff --git a/proofs/arch/arch_utils.v b/proofs/arch/arch_utils.v
index ee93b7d158..5c7fbbd86c 100644
--- a/proofs/arch/arch_utils.v
+++ b/proofs/arch/arch_utils.v
@@ -1,6 +1,6 @@
 From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat seq eqtype.
 
-Require Import
+From lang Require Import
   type
   sem_type
   strings
diff --git a/proofs/arch/arm_expand_imm.v b/proofs/arch/arm_expand_imm.v
index fd12518572..522a3593f3 100644
--- a/proofs/arch/arm_expand_imm.v
+++ b/proofs/arch/arm_expand_imm.v
@@ -4,7 +4,7 @@ From mathcomp Require Import ssreflect ssrfun ssrbool eqtype.
 From mathcomp Require Import word_ssrZ.
 
 From Coq Require Import ZArith String.
-Require Import utils word.
+From lang Require Import utils word.
 
 (* -------------------------------------------------------------------- *)
 (* Valid immediates checks. *)
diff --git a/proofs/arch/dune b/proofs/arch/dune
new file mode 100644
index 0000000000..c22527cff8
--- /dev/null
+++ b/proofs/arch/dune
@@ -0,0 +1,3 @@
+(coq.theory
+  (name arch)
+  (theories ssrmisc lang))
diff --git a/proofs/arch/sem_params_of_arch_extra.v b/proofs/arch/sem_params_of_arch_extra.v
index 1562dc4d73..6a0c6a9765 100644
--- a/proofs/arch/sem_params_of_arch_extra.v
+++ b/proofs/arch/sem_params_of_arch_extra.v
@@ -1,4 +1,4 @@
-Require Import
+From lang Require Import
   sem_params
   syscall.
 Require Import
diff --git a/proofs/common/_CoqProject b/proofs/common/_CoqProject
new file mode 100644
index 0000000000..b189c166c2
--- /dev/null
+++ b/proofs/common/_CoqProject
@@ -0,0 +1,17 @@
+-R ../_build/default/common common
+
+-arg "-set" -arg "'Uniform Inductive Parameters'"
+-arg "-set" -arg "'Implicit Arguments'"
+-arg "-unset" -arg "'Strict Implicit'"
+-arg "-unset" -arg "'Printing Implicit Defensive'"
+-arg "-w -notation-overridden"
+-arg "-w -extraction-reserved-identifier"
+-arg "-w -extraction-opaque-accessed"
+-arg "-w -ambiguous-paths"
+-arg "-w -redundant-canonical-projection"
+-arg "-w -projection-no-head-constant"
+-arg "-w -postfix-notation-not-level-1"
+-arg "-w -deprecated-since-mathcomp-2.3.0"
+-arg "-w -deprecated-since-mathcomp-2.4.0"
+-arg "-w -deprecated-from-Coq"
+-arg "-w -deprecated-dirpath-Coq"
diff --git a/proofs/common/dune b/proofs/common/dune
new file mode 100644
index 0000000000..52f265323d
--- /dev/null
+++ b/proofs/common/dune
@@ -0,0 +1,3 @@
+(coq.theory
+  (name common)
+  (theories mathcomp))
diff --git a/proofs/common/result.v b/proofs/common/result.v
new file mode 100644
index 0000000000..444b7b5d03
--- /dev/null
+++ b/proofs/common/result.v
@@ -0,0 +1,100 @@
+From mathcomp Require Import ssreflect ssrfun ssrbool.
+From Coq.Unicode Require Import Utf8.
+
+(* ** Result monad
+ * -------------------------------------------------------------------- *)
+
+Variant result (E : Type) (A : Type) : Type :=
+| Ok of A
+| Error of E.
+
+Arguments Error {E} {A} s.
+
+Definition is_ok (E A:Type) (r:result E A) := if r is Ok a then true else false.
+
+Lemma is_ok_ok (E A:Type) (a:A) : is_ok (Ok E a).
+Proof. done. Qed.
+#[global]
+Hint Resolve is_ok_ok : core.
+
+Lemma is_okP (E A:Type) (r:result E A) : reflect (exists (a:A), r = Ok E a) (is_ok r).
+Proof.
+  case: r => /=; constructor; first by eauto.
+  by move=> [].
+Qed.
+
+Module Result.
+
+Definition apply eT aT rT (f : aT -> rT) (x : rT) (u : result eT aT) :=
+  if u is Ok y then f y else x.
+
+Definition bind eT aT rT (f : aT -> result eT rT) g :=
+  match g with
+  | Ok x    => f x
+  | Error s => Error s
+  end.
+
+Definition map eT aT rT (f : aT -> rT) := bind (fun x => Ok eT (f x)).
+Definition default eT aT := @apply eT aT aT (fun x => x).
+
+Definition map_err
+  eT1 eT2 aT (f : eT1 -> eT2) (r : result eT1 aT) : result eT2 aT :=
+  match r with
+  | Ok x => Ok _ x
+  | Error e => Error (f e)
+  end.
+
+End Result.
+
+Definition o2r eT aT (e : eT) (o : option aT) :=
+  match o with
+  | None   => Error e
+  | Some x => Ok eT x
+  end.
+
+Notation rapp  := Result.apply.
+Notation rdflt := Result.default.
+Notation rbind := Result.bind.
+Notation rmap  := Result.map.
+Notation ok    := (@Ok _).
+
+Declare Scope result_scope.
+Delimit Scope result_scope with result.
+Open Scope result_scope.
+
+Notation "m >>= f" := (rbind f m) (at level 58, left associativity) : result_scope.
+Notation "'Let' x ':=' m 'in' body" := (m >>= (fun x => body)) (x name, at level 25) : result_scope.
+Notation "'Let:' x ':=' m 'in' body" := (m >>= (fun x => body)) (x strict pattern, at level 25) : result_scope.
+Notation "m >> n" := (rbind (λ _, n) m) (at level 30, right associativity, n at next level) : result_scope.
+
+Lemma bindA eT aT bT cT (f : aT -> result eT bT) (g: bT -> result eT cT) m:
+  m >>= f >>= g = m >>= (fun a => f a >>= g).
+Proof. case:m => //=. Qed.
+
+Lemma bind_eq eT aT rT (f1 f2 : aT -> result eT rT) m1 m2 :
+   m1 = m2 -> f1 =1 f2 -> m1 >>= f1 = m2 >>= f2.
+Proof. move=> <- Hf; case m1 => //=. Qed.
+
+Definition ok_inj {E A} {a a': A} (H: Ok E a = ok a') : a = a' :=
+  let 'Logic.eq_refl := H in Logic.eq_refl.
+
+Definition Error_inj {E A} (a a': E) (H: @Error E A a = Error a') : a = a' :=
+  let 'Logic.eq_refl := H in Logic.eq_refl.
+
+Definition assert E (b: bool) (e: E) : result E unit :=
+  if b then ok tt else Error e.
+
+Lemma assertP E b e u :
+  @assert E b e = ok u → b.
+Proof. by case: b. Qed.
+
+Arguments assertP {E b e u} _.
+
+Lemma map_errP eT1 eT2 aT (f : eT1 -> eT2) (r : result eT1 aT) x :
+  Result.map_err f r = ok x ->
+  r = ok x.
+Proof. by case: r => //= ? [->]. Qed.
+Arguments map_errP {_ _ _ _ _ _}.
+
+Variant error :=
+ | ErrOob | ErrAddrUndef | ErrAddrInvalid | ErrStack | ErrType | ErrArith | ErrSemUndef.
diff --git a/proofs/compiler/_CoqProject b/proofs/compiler/_CoqProject
new file mode 100644
index 0000000000..49bcec38aa
--- /dev/null
+++ b/proofs/compiler/_CoqProject
@@ -0,0 +1,24 @@
+-R ../_build/default/arch arch
+-R ../_build/default/common common
+-R ../_build/default/lang lang
+-R ../_build/default/itrees itrees
+-R ../_build/default/ssrmisc ssrmisc
+-R ../_build/default/thirdparty thirdparty
+
+-R ../_build/default/compiler compiler
+
+-arg "-set" -arg "'Uniform Inductive Parameters'"
+-arg "-set" -arg "'Implicit Arguments'"
+-arg "-unset" -arg "'Strict Implicit'"
+-arg "-unset" -arg "'Printing Implicit Defensive'"
+-arg "-w -notation-overridden"
+-arg "-w -extraction-reserved-identifier"
+-arg "-w -extraction-opaque-accessed"
+-arg "-w -ambiguous-paths"
+-arg "-w -redundant-canonical-projection"
+-arg "-w -projection-no-head-constant"
+-arg "-w -postfix-notation-not-level-1"
+-arg "-w -deprecated-since-mathcomp-2.3.0"
+-arg "-w -deprecated-since-mathcomp-2.4.0"
+-arg "-w -deprecated-from-Coq"
+-arg "-w -deprecated-dirpath-Coq"
diff --git a/proofs/compiler/allocation.v b/proofs/compiler/allocation.v
index be4fcea380..4bde29a50d 100644
--- a/proofs/compiler/allocation.v
+++ b/proofs/compiler/allocation.v
@@ -2,7 +2,8 @@
 From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat eqtype.
 From mathcomp Require Import word_ssrZ.
 From Coq Require Import ZArith.
-Require Import expr compiler_util.
+From lang Require Import expr.
+Require Import compiler_util.
 Import Utf8.
 
 Module E.
diff --git a/proofs/compiler/allocation_proof.v b/proofs/compiler/allocation_proof.v
index ec5b4067b9..b2d986f677 100644
--- a/proofs/compiler/allocation_proof.v
+++ b/proofs/compiler/allocation_proof.v
@@ -1,6 +1,7 @@
 (* ** Imports and settings *)
 From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat eqtype.
-Require Import psem compiler_util.
+From lang Require Import psem.
+Require Import compiler_util.
 Require Export allocation.
 
 Import Utf8.
diff --git a/proofs/compiler/arch_params.v b/proofs/compiler/arch_params.v
index 1181934dad..a5c6cf694c 100644
--- a/proofs/compiler/arch_params.v
+++ b/proofs/compiler/arch_params.v
@@ -1,9 +1,9 @@
-Require Import
-  compiler_util
-  expr.
-Require Import
+From lang Require Import expr.
+From arch Require Import
   arch_decl
   arch_extra.
+Require Import
+  compiler_util.
 Require
   linearization
   lowering
diff --git a/proofs/compiler/arch_params_proof.v b/proofs/compiler/arch_params_proof.v
index 4ce7a932a4..f129dccc91 100644
--- a/proofs/compiler/arch_params_proof.v
+++ b/proofs/compiler/arch_params_proof.v
@@ -1,16 +1,15 @@
 From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat eqtype.
-Require Import
-  compiler_util
+From lang Require Import
   expr
   psem.
-Require Import
+From arch Require Import
   arch_decl
   arch_extra
   arch_sem
-  asm_gen
-  asm_gen_proof
   sem_params_of_arch_extra.
+Require Import compiler_util.
 Require
+  asm_gen_proof
   linearization_proof
   lowering
   stack_alloc_params_proof
@@ -119,7 +118,7 @@ Record h_architecture_params
     hap_hlap : h_lower_addressing_params (ap_lap aparams);
 
     (* Assembly generation hypotheses. See [asm_gen_proof.v]. *)
-    hap_hagp : h_asm_gen_params (ap_agp aparams);
+    hap_hagp : asm_gen_proof.h_asm_gen_params (ap_agp aparams);
 
     (* Speculative execution lowering hypothesis *)
     hap_hshp : slh_lowering_proof.h_sh_params (ap_shp aparams);
diff --git a/proofs/compiler/armv7/_CoqProject b/proofs/compiler/armv7/_CoqProject
new file mode 100644
index 0000000000..1c2a609511
--- /dev/null
+++ b/proofs/compiler/armv7/_CoqProject
@@ -0,0 +1,25 @@
+-R ../../_build/default/arch arch
+-R ../../_build/default/compiler compiler
+-R ../../_build/default/common common
+-R ../../_build/default/lang lang
+-R ../../_build/default/itrees itrees
+-R ../../_build/default/ssrmisc ssrmisc
+-R ../../_build/default/thirdparty thirdparty
+
+-R ../../_build/default/compiler/armv7 armv7
+
+-arg "-set" -arg "'Uniform Inductive Parameters'"
+-arg "-set" -arg "'Implicit Arguments'"
+-arg "-unset" -arg "'Strict Implicit'"
+-arg "-unset" -arg "'Printing Implicit Defensive'"
+-arg "-w -notation-overridden"
+-arg "-w -extraction-reserved-identifier"
+-arg "-w -extraction-opaque-accessed"
+-arg "-w -ambiguous-paths"
+-arg "-w -redundant-canonical-projection"
+-arg "-w -projection-no-head-constant"
+-arg "-w -postfix-notation-not-level-1"
+-arg "-w -deprecated-since-mathcomp-2.3.0"
+-arg "-w -deprecated-since-mathcomp-2.4.0"
+-arg "-w -deprecated-from-Coq"
+-arg "-w -deprecated-dirpath-Coq"
diff --git a/proofs/compiler/arm.v b/proofs/compiler/armv7/arm.v
similarity index 94%
rename from proofs/compiler/arm.v
rename to proofs/compiler/armv7/arm.v
index dc7f180e34..e78afb60e5 100644
--- a/proofs/compiler/arm.v
+++ b/proofs/compiler/armv7/arm.v
@@ -1,7 +1,7 @@
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype.
 
-Require Import utils.
-Require Import arch_decl.
+From lang Require Import utils.
+From arch Require Import arch_decl.
 Require Import
   arm_decl
   arm_instr_decl.
diff --git a/proofs/compiler/arm_decl.v b/proofs/compiler/armv7/arm_decl.v
similarity index 98%
rename from proofs/compiler/arm_decl.v
rename to proofs/compiler/armv7/arm_decl.v
index 8ec0b90481..16b7408eb5 100644
--- a/proofs/compiler/arm_decl.v
+++ b/proofs/compiler/armv7/arm_decl.v
@@ -2,7 +2,7 @@ From elpi.apps Require Import derive.std.
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype fintype ssralg.
 From mathcomp Require Import word_ssrZ.
 
-Require Import
+From lang Require Import
   expr
   flag_combination
   sem_type
@@ -11,11 +11,11 @@ Require Import
   utils
   wsize.
 
-Require Import
+From arch Require Import
   arch_decl
   arch_utils.
 
-Require Export arm_expand_imm.
+From arch Require Export arm_expand_imm.
 
 (* ARM Cortex-M4 architecture
 
diff --git a/proofs/compiler/arm_extra.v b/proofs/compiler/armv7/arm_extra.v
similarity index 65%
rename from proofs/compiler/arm_extra.v
rename to proofs/compiler/armv7/arm_extra.v
index fdc73438e4..1c72d85691 100644
--- a/proofs/compiler/arm_extra.v
+++ b/proofs/compiler/armv7/arm_extra.v
@@ -2,20 +2,22 @@ From elpi.apps Require Import derive.std.
 From HB Require Import structures.
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssralg.
 
-Require Import
-  compiler_util
+From lang Require Import
   expr
   fexpr
   sopn
   utils.
-Require Export
+From arch Require Export
   arch_decl
-  arch_extra
-  arm_params_core.
+  arch_extra.
+From compiler Require Import
+  compiler_util.
 Require Import
   arm_decl
   arm_instr_decl
   arm.
+Require Export
+  arm_params_core.
 
 
 #[only(eqbOK)] derive
@@ -92,93 +94,62 @@ Instance arm_extra_op_decl : asmOp arm_extra_op | 1 :=
     prim_string := [::];
   }.
 
-Module E.
-
-Definition pass_name := "asmgen"%string.
-
-Definition internal_error (ii : instr_info) (msg : string) :=
-  {|
-    pel_msg := compiler_util.pp_s msg;
-    pel_fn := None;
-    pel_fi := None;
-    pel_ii := Some ii;
-    pel_vi := None;
-    pel_pass := Some pass_name;
-    pel_internal := true;
-  |}.
-
-Definition error (ii : instr_info) (msg : string) :=
-  {|
-    pel_msg := compiler_util.pp_s msg;
-    pel_fn := None;
-    pel_fi := None;
-    pel_ii := Some ii;
-    pel_vi := None;
-    pel_pass := Some pass_name;
-    pel_internal := false;
-  |}.
-
-Definition li_condition_modified ii :=
-  error
-    ii
-    "assignment needs to be split but condition is modified by assignment".
-End E.
-
 Definition asm_args_of_opn_args
   : seq ARMFopn_core.opn_args -> seq (asm_op_msb_t * lexprs * rexprs) :=
   map (fun '(les, aop, res) => ((None, aop), les, res)).
 
-Definition uncons X (ii : instr_info) (xs : seq X) : cexec (X * seq X) :=
+Definition uncons X (xs : seq X) : result (bool * string) (X * seq X) :=
   if xs is x :: xs
   then ok (x, xs)
-  else Error (E.internal_error ii "invalid uncons").
+  else Error (true, "invalid uncons"%string).
 
 Definition uncons_LLvar
-  (ii : instr_info) (les : seq lexpr) : cexec (var_i * seq lexpr) :=
+  (les : seq lexpr) : result (bool * string) (var_i * seq lexpr) :=
   if les is LLvar x :: les
   then ok (x, les)
-  else Error (E.internal_error ii "invalid lvals").
+  else Error (true, "invalid lvals"%string).
 
 Definition uncons_rvar
-  (ii : instr_info) (res : seq rexpr) : cexec (var_i * seq rexpr) :=
+  (res : seq rexpr) : result (bool * string) (var_i * seq rexpr) :=
   if res is Rexpr (Fvar x) :: res
   then ok (x, res)
-  else Error (E.internal_error ii "invalid arguments").
+  else Error (true, "invalid arguments"%string).
 
 Definition uncons_wconst
-  (ii : instr_info) (res : seq rexpr) : cexec (Z * seq rexpr) :=
+  (res : seq rexpr) : result (bool * string) (Z * seq rexpr) :=
   if res is Rexpr (Fapp1 (Oword_of_int _) (Fconst imm)) :: res'
   then ok (imm, res')
-  else Error (E.internal_error ii "invalid arguments").
+  else Error (true, "invalid arguments"%string).
 
-Definition smart_li_args ii ws les res :=
+Definition smart_li_args ws les res :=
   (* FIXME: This check is because [ARMFopn_core.li] only works with register
      size, it should not be the case. *)
   Let _ :=
     assert
       (ws == reg_size)
-      (E.error ii "smart immediate assignment is only valid for u32 variables")
+      (false, "smart immediate assignment is only valid for u32 variables"%string)
   in
-  Let: (x, les) := uncons_LLvar ii les in
+  Let: (x, les) := uncons_LLvar les in
   Let _ :=
-    assert (vtype (v_var x) == sword ws) (E.internal_error ii "invalid type")
+    assert (vtype (v_var x) == sword ws) (true, "invalid type"%string)
   in
-  Let _ := assert (nilp les) (E.internal_error ii "invalid lvals") in
-  Let: (imm, res) := uncons_wconst ii res in
+  Let _ := assert (nilp les) (true, "invalid lvals"%string) in
+  Let: (imm, res) := uncons_wconst res in
   ok (x, imm, res).
 
-Definition assemble_smart_li ii ws les res :=
-  Let: (x, imm, _) := smart_li_args ii ws les res in
+Definition assemble_smart_li ws les res :=
+  Let: (x, imm, _) := smart_li_args ws les res in
   ok (asm_args_of_opn_args (ARMFopn_core.li x imm)).
 
 Definition assemble_smart_li_cc
-  ii ws les res : cexec (seq (asm_op_msb_t * lexprs * rexprs)) :=
-  Let: (x, imm, res) := smart_li_args ii ws les res in
-  Let: (cond, res) := uncons ii res in
+  ws les res : result (bool * string) (seq (asm_op_msb_t * lexprs * rexprs)) :=
+  Let: (x, imm, res) := smart_li_args ws les res in
+  Let: (cond, res) := uncons res in
   Let _ :=
-    assert (~~ Sv.mem x (free_vars_r cond)) (E.li_condition_modified ii)
+    assert (~~ Sv.mem x (free_vars_r cond))
+           (false, "assignment needs to be split but condition is modified by assignment"%string)
   in
-  Let: (oldx, _) := uncons_rvar ii res in
+  Let: (oldx, _) := uncons_rvar res in
   let mk '(les, ARM_op mn opts, res) :=
     let opts := set_is_conditional opts in
     ok ((None, ARM_op mn opts), les, res ++ [:: cond; rvar oldx ])
@@ -186,11 +157,11 @@ Definition assemble_smart_li_cc
   mapM mk (ARMFopn_core.li x imm).
 
 Definition assemble_extra
-           (ii: instr_info)
+           (_ii: instr_info)
            (o: arm_extra_op)
            (outx: lexprs)
            (inx: rexprs)
-           : cexec (seq (asm_op_msb_t * lexprs * rexprs)) :=
+           : result (bool * string) (seq (asm_op_msb_t * lexprs * rexprs)) :=
   match o with
   | Oarm_swap sz =>
     if (sz == U32)%CMP then
@@ -198,11 +169,11 @@ Definition assemble_extra
       | [:: LLvar x; LLvar y], [:: Rexpr (Fvar z); Rexpr (Fvar w)] =>
         (* x, y = swap(z, w) *)
         Let _ := assert (v_var x != v_var w)
-          (E.internal_error ii "bad arm swap : x = w") in
+          (true, "bad arm swap : x = w"%string) in
         Let _ := assert (v_var y != v_var x)
-          (E.internal_error ii "bad arm swap : y = x") in
+          (true, "bad arm swap : y = x"%string) in
         Let _ := assert (all (fun (x:var_i) => vtype x == sword U32) [:: x; y; z; w])
-          (E.error ii "arm swap only valid for register of type u32") in
+          (false, "arm swap only valid for register of type u32")%string in
 
         ok [:: ((None, ARM_op EOR default_opts), [:: LLvar x], [:: Rexpr (Fvar z); Rexpr (Fvar w)]);
                (* x = z ^ w *)
@@ -210,23 +181,23 @@ Definition assemble_extra
                (* y = x ^ w = z ^ w ^ w = z *)
                ((None, ARM_op EOR default_opts), [:: LLvar x], [:: Rexpr (Fvar x); Rexpr (Fvar y)])
            ]   (* x = x ^ y = z ^ w ^ z = w *)
-      | _, _ => Error (E.error ii "only register is accepted on source and destination of the swap instruction on arm")
+      | _, _ => Error (false, "only register is accepted on source and destination of the swap instruction on arm")%string
       end
     else
-      Error (E.error ii "arm swap only valid for register of type u32")
+      Error (false, "arm swap only valid for register of type u32")%string
   | Oarm_add_large_imm =>
     match outx, inx with
     | [:: LLvar x], [:: Rexpr (Fvar y); Rexpr (Fapp1 (Oword_of_int ws) (Fconst imm))] =>
       Let _ := assert (v_var x != v_var y)
-         (E.internal_error ii "bad arm_add_large_imm: invalid register") in
+         (true, "bad arm_add_large_imm: invalid register"%string) in
       Let _ := assert (all (fun (x:var_i) => vtype x == sword U32) [:: x; y])
-          (E.error ii "arm swap only valid for register of type u32") in
+          (false, "arm swap only valid for register of type u32"%string) in
       ok (asm_args_of_opn_args (ARMFopn_core.smart_addi x y imm))
     | _, _ =>
-      Error (E.internal_error ii "bad arm_add_large_imm: invalid args or dests")
+      Error (true, "bad arm_add_large_imm: invalid args or dests"%string)
     end
-  | Osmart_li ws => assemble_smart_li ii ws outx inx
-  | Osmart_li_cc ws => assemble_smart_li_cc ii ws outx inx
+  | Osmart_li ws => assemble_smart_li ws outx inx
+  | Osmart_li_cc ws => assemble_smart_li_cc ws outx inx
   end.
 
 #[ export ]
diff --git a/proofs/compiler/arm_facts.v b/proofs/compiler/armv7/arm_facts.v
similarity index 98%
rename from proofs/compiler/arm_facts.v
rename to proofs/compiler/armv7/arm_facts.v
index 724b11b6bd..7930fd947f 100644
--- a/proofs/compiler/arm_facts.v
+++ b/proofs/compiler/armv7/arm_facts.v
@@ -1,7 +1,7 @@
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssralg.
 From Coq Require Import ZArith.
 
-Require Import
+From lang Require Import
   utils
   word.
 Require Import arm_decl.
diff --git a/proofs/compiler/arm_instr_decl.v b/proofs/compiler/armv7/arm_instr_decl.v
similarity index 99%
rename from proofs/compiler/arm_instr_decl.v
rename to proofs/compiler/armv7/arm_instr_decl.v
index 66e27621db..5f74272d67 100644
--- a/proofs/compiler/arm_instr_decl.v
+++ b/proofs/compiler/armv7/arm_instr_decl.v
@@ -7,16 +7,16 @@ From elpi.apps Require Import derive.std.
 From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat seq eqtype fintype.
 From mathcomp Require Import ssralg word_ssrZ.
 
-Require Import
+From thirdparty Require xseq.
+From lang Require Import
   sem_type
   shift_kind
   strings
   utils
-  word.
-Require xseq.
-Require Import
+  word
   values
-  sopn
+  sopn.
+From arch Require Import
   arch_decl
   arch_utils.
 Require Import arm_decl.
diff --git a/proofs/compiler/arm_instr_decl_lemmas.v b/proofs/compiler/armv7/arm_instr_decl_lemmas.v
similarity index 99%
rename from proofs/compiler/arm_instr_decl_lemmas.v
rename to proofs/compiler/armv7/arm_instr_decl_lemmas.v
index 7f4713b055..8910b12500 100644
--- a/proofs/compiler/arm_instr_decl_lemmas.v
+++ b/proofs/compiler/armv7/arm_instr_decl_lemmas.v
@@ -1,10 +1,10 @@
 From mathcomp Require Import ssreflect ssrfun ssrbool.
 From mathcomp Require Import word_ssrZ.
 
-Require Import
+From lang Require Import
   psem
   shift_kind.
-Require Import
+From arch Require Import
   arch_utils
   sem_params_of_arch_extra.
 Require Import
diff --git a/proofs/compiler/arm_lowering.v b/proofs/compiler/armv7/arm_lowering.v
similarity index 99%
rename from proofs/compiler/arm_lowering.v
rename to proofs/compiler/armv7/arm_lowering.v
index 45e3be12f7..e65c9a5c37 100644
--- a/proofs/compiler/arm_lowering.v
+++ b/proofs/compiler/armv7/arm_lowering.v
@@ -1,15 +1,16 @@
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssralg.
 From mathcomp Require Import word_ssrZ.
 
-Require Import
-  compiler_util
+From lang Require Import
   expr
-  lowering
   pseudo_operator
   shift_kind.
-Require Import
+From arch Require Import
   arch_decl
   arch_extra.
+From compiler Require Import
+  compiler_util
+  lowering.
 Require Import
   arm_decl
   arm_extra
diff --git a/proofs/compiler/arm_lowering_proof.v b/proofs/compiler/armv7/arm_lowering_proof.v
similarity index 99%
rename from proofs/compiler/arm_lowering_proof.v
rename to proofs/compiler/armv7/arm_lowering_proof.v
index f2f03a6120..4bb28a6ef7 100644
--- a/proofs/compiler/arm_lowering_proof.v
+++ b/proofs/compiler/armv7/arm_lowering_proof.v
@@ -6,16 +6,17 @@ From mathcomp Require Import word_ssrZ.
 
 From Coq Require Import Lia.
 
-Require Import
-  compiler_util
+From lang Require Import
   expr
-  lowering
-  lowering_lemmas
   psem
   utils.
-Require Import
+From arch Require Import
   arch_extra
   sem_params_of_arch_extra.
+From compiler Require Import
+  compiler_util
+  lowering
+  lowering_lemmas.
 Require Import
   arm_decl
   arm_extra
diff --git a/proofs/compiler/arm_params.v b/proofs/compiler/armv7/arm_params.v
similarity index 98%
rename from proofs/compiler/arm_params.v
rename to proofs/compiler/armv7/arm_params.v
index 1a84e32eee..0d29d43edd 100644
--- a/proofs/compiler/arm_params.v
+++ b/proofs/compiler/armv7/arm_params.v
@@ -1,23 +1,23 @@
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype.
 From mathcomp Require Import word_ssrZ.
 
-Require Import
-  arch_params
-  compiler_util
+From lang Require Import
   expr
   fexpr
   shift_kind.
-Require Import
+From arch Require Import
+  arch_decl
+  arch_extra.
+From compiler Require Import
+  arch_params
+  asm_gen
+  compiler_util
   lea
   linearization
   lowering
   stack_alloc_params
   stack_zeroization
   slh_lowering.
-Require Import
-  arch_decl
-  arch_extra
-  asm_gen.
 Require Import
   arm_decl
   arm_extra
diff --git a/proofs/compiler/arm_params_common.v b/proofs/compiler/armv7/arm_params_common.v
similarity index 95%
rename from proofs/compiler/arm_params_common.v
rename to proofs/compiler/armv7/arm_params_common.v
index dee493bcb9..7dbc1e17b1 100644
--- a/proofs/compiler/arm_params_common.v
+++ b/proofs/compiler/armv7/arm_params_common.v
@@ -1,15 +1,16 @@
 From mathcomp Require Import ssreflect ssrfun ssrbool.
 From mathcomp Require Import word_ssrZ.
 
-Require Import
-  arch_params
-  compiler_util
+From lang Require Import
   expr
   fexpr
   linear.
-Require Import
+From arch Require Import
   arch_decl
   arch_extra.
+From compiler Require Import
+  arch_params
+  compiler_util.
 Require Import
   arm_decl
   arm_extra
diff --git a/proofs/compiler/arm_params_common_proof.v b/proofs/compiler/armv7/arm_params_common_proof.v
similarity index 99%
rename from proofs/compiler/arm_params_common_proof.v
rename to proofs/compiler/armv7/arm_params_common_proof.v
index 14f3d46756..8b5e43154f 100644
--- a/proofs/compiler/arm_params_common_proof.v
+++ b/proofs/compiler/armv7/arm_params_common_proof.v
@@ -2,9 +2,7 @@ From Coq Require Import Lia.
 From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat eqtype ssralg.
 From mathcomp Require Import word_ssrZ.
 
-Require Import
-  arch_params
-  compiler_util
+From lang Require Import
   expr
   fexpr
   fexpr_sem
@@ -12,10 +10,13 @@ Require Import
   linear_sem
   linear_facts
   psem.
-Require Import
+From arch Require Import
   arch_decl
   arch_extra
   sem_params_of_arch_extra.
+From compiler Require Import
+  compiler_util
+  arch_params.
 Require Import
   arm_decl
   arm_extra
diff --git a/proofs/compiler/arm_params_core.v b/proofs/compiler/armv7/arm_params_core.v
similarity index 97%
rename from proofs/compiler/arm_params_core.v
rename to proofs/compiler/armv7/arm_params_core.v
index d774c534dd..7fca71edf0 100644
--- a/proofs/compiler/arm_params_core.v
+++ b/proofs/compiler/armv7/arm_params_core.v
@@ -1,13 +1,14 @@
 From mathcomp Require Import ssreflect ssrfun ssrbool seq eqtype.
 From mathcomp Require Import word_ssrZ.
 
-Require Import
-  compiler_util
+From lang Require Import
   expr
   fexpr
   linear.
-Require Import
+From arch Require Import
   arch_decl.
+From compiler Require Import
+  compiler_util.
 Require Import
   arm_decl
   arm_instr_decl.
diff --git a/proofs/compiler/arm_params_core_proof.v b/proofs/compiler/armv7/arm_params_core_proof.v
similarity index 99%
rename from proofs/compiler/arm_params_core_proof.v
rename to proofs/compiler/armv7/arm_params_core_proof.v
index a3d9355d98..afc4fd4eb5 100644
--- a/proofs/compiler/arm_params_core_proof.v
+++ b/proofs/compiler/armv7/arm_params_core_proof.v
@@ -2,9 +2,7 @@ From Coq Require Import Lia.
 From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat seq eqtype ssralg.
 From mathcomp Require Import word_ssrZ.
 
-Require Import
-  arch_params
-  compiler_util
+From lang Require Import
   expr
   fexpr
   fexpr_sem
@@ -12,9 +10,12 @@ Require Import
   linear_sem
   linear_facts
   psem.
-Require Import
+From arch Require Import
   arch_decl
   arch_sem.
+From compiler Require Import
+  arch_params
+  compiler_util.
 
 Require Import
   arm_decl
diff --git a/proofs/compiler/arm_params_proof.v b/proofs/compiler/armv7/arm_params_proof.v
similarity index 98%
rename from proofs/compiler/arm_params_proof.v
rename to proofs/compiler/armv7/arm_params_proof.v
index f45ee39bab..f1cd9494dc 100644
--- a/proofs/compiler/arm_params_proof.v
+++ b/proofs/compiler/armv7/arm_params_proof.v
@@ -3,32 +3,34 @@ From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat finfun.
 From mathcomp Require Import ssralg.
 From mathcomp Require Import word_ssrZ.
 
-Require Import oseq.
+From ssrmisc Require Import oseq.
 
-Require Import
-  arch_params_proof
-  compiler_util
+From lang Require Import
   expr
   fexpr
   fexpr_sem
   psem
   psem_facts
-  sem_one_varmap.
-Require Import
+  sem_one_varmap
+  linear_sem
+  linear_facts.
+From arch Require
+  arch_sem.
+From arch Require Import
+  arch_decl
+  arch_extra
+  sem_params_of_arch_extra.
+From compiler Require Import
+  arch_params_proof
+  asm_gen
+  asm_gen_proof
+  compiler_util
   lea_proof
   linearization
   linearization_proof
   lowering
   stack_alloc_params_proof
   stack_zeroization_proof.
-Require
-  arch_sem.
-Require Import
-  arch_decl
-  arch_extra
-  asm_gen
-  asm_gen_proof
-  sem_params_of_arch_extra.
 Require Import
   arm_decl
   arm_extra
@@ -224,7 +226,7 @@ Qed.
 Lemma arm_spec_lip_set_up_sp_register :
   set_up_sp_register_correct arm_liparams.
 Proof.
-  Opaque sem_fopn_args.
+  Opaque linear_sem.sem_fopn_args.
   move=> [[? nrsp] vi1] [[? nr] vi2] [[? ntmp] vi3] ts al sz s hget /= ??? hne hne1 hne2; subst.
   rewrite /arm_set_up_sp_register sem_fopns_args_cat /=.
   set vr := {|vname := nr|}; set r := {|v_var := vr|}.
@@ -722,30 +724,30 @@ Proof.
   by apply heqex; rewrite /arm_reg_size; SvD.fsetdec.
 Qed.
 
-Lemma unconsP {ii X x} {xs xs' : seq X} :
-  uncons ii xs = ok (x, xs') ->
+Lemma unconsP {X x} {xs xs' : seq X} :
+  uncons xs = ok (x, xs') ->
   xs = x :: xs'.
 Proof. by case: xs => [// | ??] [-> ->]. Qed.
 
-Lemma uncons_LLvarP ii les x les' :
-  uncons_LLvar ii les = ok (x, les') ->
+Lemma uncons_LLvarP les x les' :
+  uncons_LLvar les = ok (x, les') ->
   les = LLvar x :: les'.
 Proof. by case: les => [// | [// | ?] ?] [-> ->]. Qed.
 
-Lemma uncons_rvarP ii res x res' :
-  uncons_rvar ii res = ok (x, res') ->
+Lemma uncons_rvarP res x res' :
+  uncons_rvar res = ok (x, res') ->
   res = rvar x :: res'.
 Proof. by case: res => [// | [// | [] // ?] ?] [-> ->]. Qed.
 
-Lemma uncons_wconstP ii les imm les' :
-  uncons_wconst ii les = ok (imm, les') ->
+Lemma uncons_wconstP les imm les' :
+  uncons_wconst les = ok (imm, les') ->
   exists ws, les = rconst ws imm :: les'.
 Proof.
   case: les => [// | [//|]] [] // [] // ? [] // ?? [-> ->]. by eexists.
 Qed.
 
-Lemma smart_li_argsP ii ws les res x imm res' :
-  smart_li_args ii ws les res = ok (x, imm, res') ->
+Lemma smart_li_argsP ws les res x imm res' :
+  smart_li_args ws les res = ok (x, imm, res') ->
   [/\ ws = reg_size
     , les = [:: LLvar x ]
     , vtype (v_var x) = sword reg_size
diff --git a/proofs/compiler/arm_stack_zeroization.v b/proofs/compiler/armv7/arm_stack_zeroization.v
similarity index 96%
rename from proofs/compiler/arm_stack_zeroization.v
rename to proofs/compiler/armv7/arm_stack_zeroization.v
index a4ca6f8607..698d25d52a 100644
--- a/proofs/compiler/arm_stack_zeroization.v
+++ b/proofs/compiler/armv7/arm_stack_zeroization.v
@@ -1,18 +1,20 @@
 From mathcomp Require Import ssreflect.
 
-Require Import
+From lang Require Import
   expr
   fexpr
   label
   linear
-  stack_zero_strategy
+  stack_zero_strategy.
+From arch Require Import
   arch_decl
-  arch_extra
+  arch_extra.
+Require Import
   arm_decl
   arm_extra
   arm_instr_decl
   arm_params_common.
-Require Import compiler_util.
+From compiler Require Import compiler_util.
 
 Section STACK_ZEROIZATION.
 
diff --git a/proofs/compiler/arm_stack_zeroization_proof.v b/proofs/compiler/armv7/arm_stack_zeroization_proof.v
similarity index 99%
rename from proofs/compiler/arm_stack_zeroization_proof.v
rename to proofs/compiler/armv7/arm_stack_zeroization_proof.v
index 46b1412939..085201c3eb 100644
--- a/proofs/compiler/arm_stack_zeroization_proof.v
+++ b/proofs/compiler/armv7/arm_stack_zeroization_proof.v
@@ -2,7 +2,7 @@ From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat eqtype ssralg.
 From mathcomp Require Import word_ssrZ.
 From Coq Require Import Lia.
 
-Require Import
+From lang Require Import
   expr
   fexpr
   fexpr_sem
@@ -12,11 +12,11 @@ Require Import
   psem
   psem_facts
   low_memory.
-Require stack_zeroization_proof.
-Require Import
+From arch Require Import
   arch_decl
   arch_extra
   sem_params_of_arch_extra.
+From compiler Require stack_zeroization_proof.
 Require Import
   arm_decl
   arm_extra
diff --git a/proofs/compiler/armv7/dune b/proofs/compiler/armv7/dune
new file mode 100644
index 0000000000..e15372441d
--- /dev/null
+++ b/proofs/compiler/armv7/dune
@@ -0,0 +1,3 @@
+(coq.theory
+  (name armv7)
+  (theories ssrmisc thirdparty lang arch compiler))
diff --git a/proofs/compiler/array_copy.v b/proofs/compiler/array_copy.v
index 9e0d6a3da8..339455afaa 100644
--- a/proofs/compiler/array_copy.v
+++ b/proofs/compiler/array_copy.v
@@ -1,8 +1,9 @@
 From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat eqtype.
-Require Import
-  compiler_util
+From lang Require Import
   expr
   pseudo_operator.
+Require Import
+  compiler_util.
 Import Utf8.
 
 (*
diff --git a/proofs/compiler/array_copy_proof.v b/proofs/compiler/array_copy_proof.v
index 8aa043b4b8..1a61ffd9a8 100644
--- a/proofs/compiler/array_copy_proof.v
+++ b/proofs/compiler/array_copy_proof.v
@@ -2,7 +2,8 @@
 From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat eqtype.
 From mathcomp Require Import word_ssrZ.
 From Coq Require Import ZArith Lia.
-Require Import array_copy psem.
+From lang Require Import psem.
+Require Import array_copy.
 Require Import compiler_util.
 Import Utf8.
 
diff --git a/proofs/compiler/array_expansion.v b/proofs/compiler/array_expansion.v
index 5a6d852165..8e92168e31 100644
--- a/proofs/compiler/array_expansion.v
+++ b/proofs/compiler/array_expansion.v
@@ -3,7 +3,8 @@
 From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat eqtype.
 From mathcomp Require Import word_ssrZ.
 From Coq Require Import ZArith.
-Require Import expr compiler_util.
+From lang Require Import expr.
+Require Import compiler_util.
 Import Utf8.
 
 Local Open Scope seq_scope.
diff --git a/proofs/compiler/array_expansion_proof.v b/proofs/compiler/array_expansion_proof.v
index 3ba4032a51..c0dc8fb884 100644
--- a/proofs/compiler/array_expansion_proof.v
+++ b/proofs/compiler/array_expansion_proof.v
@@ -2,7 +2,8 @@
 From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat eqtype.
 From mathcomp Require Import word_ssrZ.
 From Coq Require Import ZArith.
-Require Import psem array_expansion compiler_util.
+From lang Require Import psem.
+Require Import array_expansion compiler_util.
 Import Utf8 Lia.
 
 Local Open Scope seq_scope.
diff --git a/proofs/compiler/array_init.v b/proofs/compiler/array_init.v
index 7d38aad1c4..58e3b7ef58 100644
--- a/proofs/compiler/array_init.v
+++ b/proofs/compiler/array_init.v
@@ -1,7 +1,8 @@
 (* ** Imports and settings *)
 From Coq Require Import ZArith.
 From mathcomp Require Import ssreflect ssrfun ssrbool.
-Require Import expr compiler_util.
+From lang Require Import expr.
+Require Import compiler_util.
 
 Local Open Scope seq_scope.
 
diff --git a/proofs/compiler/array_init_proof.v b/proofs/compiler/array_init_proof.v
index 4307a25e61..1ca388b1bf 100644
--- a/proofs/compiler/array_init_proof.v
+++ b/proofs/compiler/array_init_proof.v
@@ -1,6 +1,7 @@
 (* ** Imports and settings *)
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype.
-Require Import psem_core psem compiler_util.
+From lang Require Import psem_core psem.
+Require Import compiler_util.
 Require Export array_init.
 Import Utf8.
 
diff --git a/proofs/arch/asm_gen.v b/proofs/compiler/asm_gen.v
similarity index 98%
rename from proofs/arch/asm_gen.v
rename to proofs/compiler/asm_gen.v
index b0a8558220..6f2a54897e 100644
--- a/proofs/arch/asm_gen.v
+++ b/proofs/compiler/asm_gen.v
@@ -1,15 +1,15 @@
 From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat eqtype ssralg.
-Require Import
-  compiler_util
+From lang Require Import
   expr
   fexpr
   one_varmap
-  linear
-  lea.
-Require Import
+  linear.
+From arch Require Import
   arm_expand_imm
   arch_decl
   arch_extra.
+Require Import compiler_util.
+Require Import lea.
 Import Utf8 String.
 Import compiler_util oseq.
 
@@ -508,7 +508,10 @@ Definition assemble_sopn rip ii (op: sopn) (outx : lexprs) (inx : rexprs) :=
     Let i := assemble_asm_op rip ii op outx inx in
     ok [:: i ]
   | Oasm (ExtOp op) =>
-    Let args := to_asm ii op outx inx in
+    let mk_err '(b, s) :=
+      if b then E.internal_error ii s else E.error ii (pp_s s)
+    in
+    Let args := Result.map_err mk_err (to_asm ii op outx inx) in
     mapM (assemble_asm_args rip ii) args
   | _ => Error (E.unexpected_sopn ii "assemble_sopn:" op)
   end.
diff --git a/proofs/arch/asm_gen_proof.v b/proofs/compiler/asm_gen_proof.v
similarity index 99%
rename from proofs/arch/asm_gen_proof.v
rename to proofs/compiler/asm_gen_proof.v
index 0710a548ec..0816cf9965 100644
--- a/proofs/arch/asm_gen_proof.v
+++ b/proofs/compiler/asm_gen_proof.v
@@ -1,22 +1,22 @@
 From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat eqtype.
 From mathcomp Require Import fintype finfun ssralg.
 From Coq Require Import Relation_Operators.
-Require Import
-  compiler_util
+From lang Require Import
   psem
   psem_facts
   label
-  lea_proof
   one_varmap sem_one_varmap
   linear
   linear_sem
   fexpr
   fexpr_sem.
-Require Import
+From arch Require Import
   arch_decl
   arch_extra
   arch_sem
   sem_params_of_arch_extra.
+Require Import compiler_util.
+Require Import lea_proof.
 Require Export asm_gen.
 Import Utf8.
 Import oseq.
@@ -1121,6 +1121,7 @@ Proof.
   + move=> a h1 h2 h3; t_xrbindP => -[op' args'] h4 <- h5.
     by have [s' hs' heq] := assemble_asm_opP h1 h2 h3 h4 h5; exists s' => //=; rewrite hs'.
   t_xrbindP=> op ok_xs ok_ys hsem ops'.
+  move=> /map_errP.
   exact: (hagp_assemble_extra_op hagparams ok_xs ok_ys).
 Qed.
 
diff --git a/proofs/compiler/compiler.v b/proofs/compiler/compiler.v
index b8dae27b70..37a09103ff 100644
--- a/proofs/compiler/compiler.v
+++ b/proofs/compiler/compiler.v
@@ -5,20 +5,22 @@ From mathcomp Require Import ssralg.
 From Coq Require Import ZArith Uint63.
 From Coq Require Import Utf8.
 
-Require Import
-  arch_params
-  compiler_util
+From lang Require Import
+  wsize
   expr
   flag_combination.
-Require Import
+From arch Require Import
   arch_decl
-  arch_extra
-  asm_gen.
+  arch_extra.
+Require Import
+  arch_params
+  compiler_util.
 Require Import
   allocation
   array_copy
   array_expansion
   array_init
+  asm_gen
   constant_prop
   dead_calls
   lower_spill
@@ -36,8 +38,8 @@ Require Import
   stack_zeroization
   tunneling
   unrolling
-  wsize
   wint_word.
+Import wsize.
 
 Require
   merge_varmaps.
diff --git a/proofs/compiler/compiler_proof.v b/proofs/compiler/compiler_proof.v
index 386150609d..6662e8441b 100644
--- a/proofs/compiler/compiler_proof.v
+++ b/proofs/compiler/compiler_proof.v
@@ -2,14 +2,23 @@ From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat seq eqtype.
 From mathcomp Require Import fintype finfun ssralg.
 From Coq Require Import Uint63.
 
+From lang Require Import
+  psem
+  psem_facts
+  psem_of_sem_proof
+  linear_sem.
+From arch Require Import
+  arch_decl
+  arch_extra
+  arch_sem
+  sem_params_of_arch_extra.
 Require Import
   arch_params_proof
   compiler
-  compiler_util
-  psem
-  psem_facts.
+  compiler_util.
 Require Import
   allocation_proof
+  asm_gen_proof
   lower_spill_proof
   load_constants_in_cond_proof
   inline_proof
@@ -29,18 +38,11 @@ Require Import
   tunneling_proof
   linearization_proof
   merge_varmaps_proof
-  psem_of_sem_proof
   slh_lowering_proof
   direct_call_proof
   stack_zeroization_proof
   wint_word_proof.
 
-Require Import
-  arch_decl
-  arch_extra
-  arch_sem
-  asm_gen_proof
-  sem_params_of_arch_extra.
 Import Utf8.
 Import wsize.
 
diff --git a/proofs/compiler/compiler_util.v b/proofs/compiler/compiler_util.v
index 9fa1618c14..418e3e90c8 100644
--- a/proofs/compiler/compiler_util.v
+++ b/proofs/compiler/compiler_util.v
@@ -1,6 +1,6 @@
 From Coq Require Import ZArith Setoid Morphisms.
 From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat eqtype.
-Require Import expr fexpr.
+From lang Require Import expr fexpr.
 
 Local Unset Elimination Schemes.
 
diff --git a/proofs/compiler/constant_prop.v b/proofs/compiler/constant_prop.v
index f310c8d867..da2085a19b 100644
--- a/proofs/compiler/constant_prop.v
+++ b/proofs/compiler/constant_prop.v
@@ -3,10 +3,10 @@ From HB Require Import structures.
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssralg.
 From mathcomp Require Import word_ssrZ.
 From Coq Require Import ZArith.
-Require Import expr sem_op_typed compiler_util.
+From lang Require Import expr sem_op_typed flag_combination.
+Require Import compiler_util.
 Import Utf8.
 Import oseq.
-Require Import flag_combination.
 
 Local Open Scope seq_scope.
 Local Open Scope Z_scope.
diff --git a/proofs/compiler/constant_prop_proof.v b/proofs/compiler/constant_prop_proof.v
index 09d36c9386..7c3e821ea6 100644
--- a/proofs/compiler/constant_prop_proof.v
+++ b/proofs/compiler/constant_prop_proof.v
@@ -1,6 +1,7 @@
 (* ** Imports and settings *)
 From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat eqtype ssralg.
-Require Import psem compiler_util.
+From lang Require Import psem.
+Require Import compiler_util.
 Require Export constant_prop.
 
 Import Utf8 ZArith Morphisms Classes.RelationClasses.
diff --git a/proofs/compiler/dead_calls.v b/proofs/compiler/dead_calls.v
index dccb2b9ee7..1d86500dcf 100644
--- a/proofs/compiler/dead_calls.v
+++ b/proofs/compiler/dead_calls.v
@@ -1,6 +1,7 @@
 (* -------------------------------------------------------------------- *)
 From mathcomp Require Import ssreflect ssrfun ssrbool.
-(* ------- *) Require Import expr compiler_util gen_map.
+From lang     Require Import expr gen_map.
+(* ------- *) Require Import compiler_util.
 (* ------- *) (* - *) Import PosSet.
 Import  Utf8.
 
diff --git a/proofs/compiler/dead_calls_proof.v b/proofs/compiler/dead_calls_proof.v
index 1d245a6648..1b5a75df2d 100644
--- a/proofs/compiler/dead_calls_proof.v
+++ b/proofs/compiler/dead_calls_proof.v
@@ -1,6 +1,7 @@
 (* -------------------------------------------------------------------- *)
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype.
-(* ------- *) Require Import expr compiler_util psem gen_map dead_calls.
+From lang     Require Import expr psem gen_map.
+(* ------- *) Require Import compiler_util dead_calls.
 (* ------- *) (* - *) Import PosSet.
 Import Utf8 xseq.
 
diff --git a/proofs/compiler/dead_code.v b/proofs/compiler/dead_code.v
index 973c571538..18cf3532c0 100644
--- a/proofs/compiler/dead_code.v
+++ b/proofs/compiler/dead_code.v
@@ -1,7 +1,8 @@
 (* ** Imports and settings *)
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype.
 From Coq Require Import ZArith.
-Require Import expr compiler_util.
+From lang Require Import expr.
+Require Import compiler_util.
 
 Local Open Scope seq_scope.
 
diff --git a/proofs/compiler/dead_code_proof.v b/proofs/compiler/dead_code_proof.v
index 306b3f889b..502c353884 100644
--- a/proofs/compiler/dead_code_proof.v
+++ b/proofs/compiler/dead_code_proof.v
@@ -1,6 +1,7 @@
 (* ** Imports and settings *)
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype.
-Require Import psem compiler_util.
+From lang Require Import psem.
+Require Import compiler_util.
 Require Export dead_code.
 Import Utf8.
 
diff --git a/proofs/compiler/direct_call_proof.v b/proofs/compiler/direct_call_proof.v
index 0ecb11263a..ddf860935d 100644
--- a/proofs/compiler/direct_call_proof.v
+++ b/proofs/compiler/direct_call_proof.v
@@ -1,6 +1,6 @@
 (* ** Imports and settings *)
 From mathcomp Require Import ssreflect ssrfun ssrbool.
-Require Import varmap psem.
+From lang Require Import varmap psem.
 
 Import Utf8.
 
diff --git a/proofs/compiler/dune b/proofs/compiler/dune
new file mode 100644
index 0000000000..506db4c35f
--- /dev/null
+++ b/proofs/compiler/dune
@@ -0,0 +1,3 @@
+(coq.theory
+  (name compiler)
+  (theories ssrmisc thirdparty lang arch))
diff --git a/proofs/compiler/inline.v b/proofs/compiler/inline.v
index c322c3d571..8a253663d7 100644
--- a/proofs/compiler/inline.v
+++ b/proofs/compiler/inline.v
@@ -1,7 +1,8 @@
 (* ** Imports and settings *)
 From Coq Require Import ZArith.
 From mathcomp Require Import ssreflect ssrfun ssrbool.
-Require Import expr compiler_util allocation.
+From lang Require Import expr.
+Require Import compiler_util allocation.
 
 Local Open Scope seq_scope.
 
diff --git a/proofs/compiler/inline_proof.v b/proofs/compiler/inline_proof.v
index 53ee4ecbc4..b4b5cc3553 100644
--- a/proofs/compiler/inline_proof.v
+++ b/proofs/compiler/inline_proof.v
@@ -1,7 +1,8 @@
 (* ** Imports and settings *)
 From Coq Require Import ZArith.
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype.
-Require Import psem allocation_proof compiler_util.
+From lang Require Import psem.
+Require Import allocation_proof compiler_util.
 Require Export inline.
 
 Local Open Scope seq_scope.
diff --git a/proofs/compiler/jasmin_compiler.v b/proofs/compiler/jasmin_compiler.v
deleted file mode 100644
index 55fcaf32f2..0000000000
--- a/proofs/compiler/jasmin_compiler.v
+++ /dev/null
@@ -1,8 +0,0 @@
-(** This module is meant as the minimal dependency of extracted code. *)
-Require compiler.
-Require psem_defs.
-Require arm_params.
-Require x86_params.
-Require riscv_params.
-Require sem_params_of_arch_extra.
-Require wint_int.
diff --git a/proofs/compiler/lea.v b/proofs/compiler/lea.v
index 7ba5d8056e..c06fb0af8b 100644
--- a/proofs/compiler/lea.v
+++ b/proofs/compiler/lea.v
@@ -1,8 +1,7 @@
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype.
 From mathcomp Require Import word_ssrZ.
 From Coq Require Import Utf8.
-Require Import expr.
-Require Import fexpr.
+From lang Require Import expr fexpr.
 
 (* -------------------------------------------------------------------- *)
 
diff --git a/proofs/compiler/lea_proof.v b/proofs/compiler/lea_proof.v
index f1ec287a36..cceae87050 100644
--- a/proofs/compiler/lea_proof.v
+++ b/proofs/compiler/lea_proof.v
@@ -1,8 +1,8 @@
 (* ** Imports and settings *)
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat ssralg.
-Require Import oseq.
-Require Import psem compiler_util.
-Require Import fexpr fexpr_sem fexpr_facts.
+From ssrmisc Require Import oseq.
+From lang Require Import psem fexpr fexpr_sem fexpr_facts.
+Require Import compiler_util.
 Require Export lea.
 Import Utf8.
 Import ssrring.
diff --git a/proofs/compiler/linear_util.v b/proofs/compiler/linear_util.v
index 03712a8ae5..c1f45fafa8 100644
--- a/proofs/compiler/linear_util.v
+++ b/proofs/compiler/linear_util.v
@@ -1,6 +1,7 @@
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype.
-Require Import expr label linear.
-Require Import seq_extra compiler_util.
+From lang Require Import expr label linear.
+From ssrmisc Require Import seq_extra.
+Require Import compiler_util.
 
 (* [map_cfprog_gen] specialized to functions of type [lfundef] *)
 Notation map_cflprog_name := (map_cfprog_name_gen lfd_info).
diff --git a/proofs/compiler/linearization.v b/proofs/compiler/linearization.v
index 2ae7a79f63..91c79c243e 100644
--- a/proofs/compiler/linearization.v
+++ b/proofs/compiler/linearization.v
@@ -6,8 +6,11 @@ From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat seq eqtype.
 From Coq Require Import ZArith Utf8.
 Import Relations.
 
-Require Import expr fexpr compiler_util label constant_prop.
-Require Export linear linear_util.
+From lang Require Import expr fexpr label.
+From lang Require Export linear.
+Require Import compiler_util.
+Require Export linear_util.
+Require Import constant_prop.
 Import word_ssrZ.
 
 Local Open Scope seq_scope.
diff --git a/proofs/compiler/linearization_proof.v b/proofs/compiler/linearization_proof.v
index b7d48e6d1b..ca72be9df2 100644
--- a/proofs/compiler/linearization_proof.v
+++ b/proofs/compiler/linearization_proof.v
@@ -6,14 +6,15 @@ From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat seq eqtype ssralg.
 From Coq Require Import ZArith Utf8.
 Import Relations.
 
-Require sem_one_varmap_facts label.
+From lang Require sem_one_varmap_facts label.
 Import word_ssrZ.
 Import ssrring.
-Import psem psem_facts sem_one_varmap compiler_util label sem_one_varmap_facts low_memory.
-Require Import seq_extra.
+Import psem psem_facts sem_one_varmap label sem_one_varmap_facts low_memory.
+From ssrmisc Require Import seq_extra.
+Require Import compiler_util.
 Require Import constant_prop constant_prop_proof.
-Require Import fexpr fexpr_sem fexpr_facts.
-Require Export linearization linear_sem linear_facts.
+From lang Require Import fexpr fexpr_sem fexpr_facts linear_sem linear_facts.
+Require Export linearization.
 Import Memory.
 
 #[local] Existing Instance withsubword.
diff --git a/proofs/compiler/load_constants_in_cond.v b/proofs/compiler/load_constants_in_cond.v
index 0a6775cb80..d4dc0a97ec 100644
--- a/proofs/compiler/load_constants_in_cond.v
+++ b/proofs/compiler/load_constants_in_cond.v
@@ -1,7 +1,8 @@
 (* ** Imports and settings *)
 From mathcomp Require Import ssreflect ssrfun ssrbool.
 From Coq Require Import Uint63.
-Require Import expr compiler_util.
+From lang Require Import expr.
+Require Import compiler_util.
 
 Local Open Scope seq_scope.
 
diff --git a/proofs/compiler/load_constants_in_cond_proof.v b/proofs/compiler/load_constants_in_cond_proof.v
index b5271c48d4..58c90fd1a3 100644
--- a/proofs/compiler/load_constants_in_cond_proof.v
+++ b/proofs/compiler/load_constants_in_cond_proof.v
@@ -1,7 +1,8 @@
 (* ** Imports and settings *)
 From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat eqtype.
 From Coq Require Import Uint63.
-Require Import psem compiler_util.
+From lang Require Import psem.
+Require Import compiler_util.
 Require Export load_constants_in_cond.
 Import Utf8.
 
diff --git a/proofs/compiler/lower_spill.v b/proofs/compiler/lower_spill.v
index 30888ab219..c29b047ab4 100644
--- a/proofs/compiler/lower_spill.v
+++ b/proofs/compiler/lower_spill.v
@@ -1,7 +1,8 @@
 (* ** Imports and settings *)
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype.
 From Coq Require Import ZArith.
-Require Import pseudo_operator expr compiler_util.
+From lang Require Import pseudo_operator expr.
+Require Import compiler_util.
 
 Local Open Scope seq_scope.
 
diff --git a/proofs/compiler/lower_spill_proof.v b/proofs/compiler/lower_spill_proof.v
index a75bc02ecb..8dcc1d2ebc 100644
--- a/proofs/compiler/lower_spill_proof.v
+++ b/proofs/compiler/lower_spill_proof.v
@@ -1,7 +1,8 @@
 (* ** Imports and settings *)
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype.
-Require Import psem compiler_util.
-Require Export pseudo_operator lower_spill.
+From lang Require Import psem pseudo_operator.
+Require Import compiler_util.
+Require Export lower_spill.
 Import Utf8.
 
 Local Open Scope seq_scope.
diff --git a/proofs/compiler/lowering.v b/proofs/compiler/lowering.v
index 2268622e00..c5f68f1bbe 100644
--- a/proofs/compiler/lowering.v
+++ b/proofs/compiler/lowering.v
@@ -1,4 +1,5 @@
-Require Import compiler_util expr.
+From lang Require Import expr.
+Require Import compiler_util.
 
 Section LOWERING.
 
diff --git a/proofs/lang/lowering_lemmas.v b/proofs/compiler/lowering_lemmas.v
similarity index 99%
rename from proofs/lang/lowering_lemmas.v
rename to proofs/compiler/lowering_lemmas.v
index ae5ddefd7a..f8aba656fe 100644
--- a/proofs/lang/lowering_lemmas.v
+++ b/proofs/compiler/lowering_lemmas.v
@@ -1,11 +1,11 @@
 From mathcomp Require Import ssreflect ssrfun ssrbool.
 
-Require Import
+From lang Require Import
   expr
   low_memory
-  lowering
   psem.
-
+Require Import
+  lowering.
 
 Section ESTATE_EQ_EXCEPT.
 
diff --git a/proofs/compiler/makeReferenceArguments.v b/proofs/compiler/makeReferenceArguments.v
index d24473337a..cc2829934f 100644
--- a/proofs/compiler/makeReferenceArguments.v
+++ b/proofs/compiler/makeReferenceArguments.v
@@ -1,7 +1,8 @@
 (* ** Imports and settings *)
 From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat.
 From Coq Require Import ZArith Uint63.
-Require Import gen_map expr compiler_util.
+From lang Require Import gen_map expr.
+Require Import compiler_util.
 
 Local Open Scope seq_scope.
 
diff --git a/proofs/compiler/makeReferenceArguments_proof.v b/proofs/compiler/makeReferenceArguments_proof.v
index a1a7f6e0a1..b29fee68e4 100644
--- a/proofs/compiler/makeReferenceArguments_proof.v
+++ b/proofs/compiler/makeReferenceArguments_proof.v
@@ -1,7 +1,8 @@
 (* ** Imports and settings *)
 From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat eqtype.
 From Coq Require Import Uint63.
-Require Import psem compiler_util.
+From lang Require Import psem.
+Require Import compiler_util.
 Require Export makeReferenceArguments.
 Import Utf8.
 
diff --git a/proofs/compiler/merge_varmaps.v b/proofs/compiler/merge_varmaps.v
index 5ba211c025..51217f0d36 100644
--- a/proofs/compiler/merge_varmaps.v
+++ b/proofs/compiler/merge_varmaps.v
@@ -1,9 +1,9 @@
 (*
 *)
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype.
-Require Import one_varmap.
+From lang Require Import expr one_varmap.
+Require Import compiler_util.
 Import Utf8.
-Import expr compiler_util.
 
 (** This is a checker that it is safe to merge the local variables of a function and its caller.
 
diff --git a/proofs/compiler/merge_varmaps_proof.v b/proofs/compiler/merge_varmaps_proof.v
index 496f6407a8..0da0366fe3 100644
--- a/proofs/compiler/merge_varmaps_proof.v
+++ b/proofs/compiler/merge_varmaps_proof.v
@@ -1,8 +1,9 @@
 (*
 *)
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssralg.
-Require Import sem_one_varmap sem_one_varmap_facts merge_varmaps psem_facts.
-Require Import seq_extra.
+From lang Require Import sem_one_varmap sem_one_varmap_facts psem_facts.
+From ssrmisc Require Import seq_extra.
+Require Import merge_varmaps.
 Import Utf8.
 Import word_ssrZ.
 Import psem.
diff --git a/proofs/compiler/post_unrolling_check.v b/proofs/compiler/post_unrolling_check.v
index adf65c4dfe..840d09a72e 100644
--- a/proofs/compiler/post_unrolling_check.v
+++ b/proofs/compiler/post_unrolling_check.v
@@ -1,5 +1,6 @@
 From mathcomp Require Import ssreflect.
-Require Import expr compiler_util.
+From lang Require Import expr.
+Require Import compiler_util.
 
 Import Utf8.
 
diff --git a/proofs/compiler/propagate_inline.v b/proofs/compiler/propagate_inline.v
index 8562b0c6e6..c390ea2cbc 100644
--- a/proofs/compiler/propagate_inline.v
+++ b/proofs/compiler/propagate_inline.v
@@ -2,9 +2,8 @@
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype.
 From mathcomp Require Import word_ssrZ.
 From Coq Require Import ZArith.
-Require Import compiler_util expr constant_prop.
-Require Import
-  flag_combination.
+From lang Require Import expr flag_combination.
+Require Import compiler_util constant_prop.
 Import Utf8.
 
 Module Import E.
diff --git a/proofs/compiler/propagate_inline_proof.v b/proofs/compiler/propagate_inline_proof.v
index 02aa0cbca5..29e96a93ca 100644
--- a/proofs/compiler/propagate_inline_proof.v
+++ b/proofs/compiler/propagate_inline_proof.v
@@ -1,6 +1,7 @@
 (* ** Imports and settings *)
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype.
-Require Import psem psem_facts constant_prop constant_prop_proof.
+From lang Require Import psem psem_facts.
+Require Import constant_prop constant_prop_proof.
 Require Export propagate_inline.
 
 Import Utf8 ZArith Morphisms Classes.RelationClasses.
diff --git a/proofs/compiler/remove_globals.v b/proofs/compiler/remove_globals.v
index 4ccc2a49b4..7a5c4cfda2 100644
--- a/proofs/compiler/remove_globals.v
+++ b/proofs/compiler/remove_globals.v
@@ -2,8 +2,9 @@
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssralg.
 From mathcomp Require Import word_ssrZ.
 From Coq Require Import ZArith.
-Require Import xseq.
-Require Import expr compiler_util.
+From thirdparty Require Import xseq.
+From lang Require Import expr.
+Require Import compiler_util.
 
 Local Open Scope seq_scope.
 
diff --git a/proofs/compiler/remove_globals_proof.v b/proofs/compiler/remove_globals_proof.v
index a50f7b27b8..570a2e5d7e 100644
--- a/proofs/compiler/remove_globals_proof.v
+++ b/proofs/compiler/remove_globals_proof.v
@@ -2,8 +2,9 @@
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssralg.
 From mathcomp Require Import word_ssrZ.
 From Coq Require Import ZArith.
-Require Import xseq.
-Require Import compiler_util expr psem remove_globals low_memory.
+From thirdparty Require Import xseq.
+From lang Require Import expr psem low_memory.
+Require Import compiler_util remove_globals.
 Import Utf8.
 
 Definition gd_incl (gd1 gd2: glob_decls) :=
diff --git a/proofs/compiler/riscv/_CoqProject b/proofs/compiler/riscv/_CoqProject
new file mode 100644
index 0000000000..f445895dcf
--- /dev/null
+++ b/proofs/compiler/riscv/_CoqProject
@@ -0,0 +1,25 @@
+-R ../../_build/default/arch arch
+-R ../../_build/default/compiler compiler
+-R ../../_build/default/common common
+-R ../../_build/default/lang lang
+-R ../../_build/default/itrees itrees
+-R ../../_build/default/ssrmisc ssrmisc
+-R ../../_build/default/thirdparty thirdparty
+
+-R ../../_build/default/compiler/riscv riscv
+
+-arg "-set" -arg "'Uniform Inductive Parameters'"
+-arg "-set" -arg "'Implicit Arguments'"
+-arg "-unset" -arg "'Strict Implicit'"
+-arg "-unset" -arg "'Printing Implicit Defensive'"
+-arg "-w -notation-overridden"
+-arg "-w -extraction-reserved-identifier"
+-arg "-w -extraction-opaque-accessed"
+-arg "-w -ambiguous-paths"
+-arg "-w -redundant-canonical-projection"
+-arg "-w -projection-no-head-constant"
+-arg "-w -postfix-notation-not-level-1"
+-arg "-w -deprecated-since-mathcomp-2.3.0"
+-arg "-w -deprecated-since-mathcomp-2.4.0"
+-arg "-w -deprecated-from-Coq"
+-arg "-w -deprecated-dirpath-Coq"
diff --git a/proofs/compiler/riscv/dune b/proofs/compiler/riscv/dune
new file mode 100644
index 0000000000..1249174c79
--- /dev/null
+++ b/proofs/compiler/riscv/dune
@@ -0,0 +1,3 @@
+(coq.theory
+  (name riscv)
+  (theories ssrmisc thirdparty lang arch compiler))
diff --git a/proofs/compiler/riscv.v b/proofs/compiler/riscv/riscv.v
similarity index 93%
rename from proofs/compiler/riscv.v
rename to proofs/compiler/riscv/riscv.v
index 7b893c1275..d6d376afd2 100644
--- a/proofs/compiler/riscv.v
+++ b/proofs/compiler/riscv/riscv.v
@@ -1,10 +1,10 @@
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssralg.
 From Coq Require Import
   ZArith.
-Require Import
+From lang Require Import
   utils
   word.
-Require Import arch_decl.
+From arch Require Import arch_decl.
 Require Import
   riscv_decl
   riscv_instr_decl.
diff --git a/proofs/compiler/riscv_decl.v b/proofs/compiler/riscv/riscv_decl.v
similarity index 98%
rename from proofs/compiler/riscv_decl.v
rename to proofs/compiler/riscv/riscv_decl.v
index 755cfe0441..28f402de8d 100644
--- a/proofs/compiler/riscv_decl.v
+++ b/proofs/compiler/riscv/riscv_decl.v
@@ -2,7 +2,7 @@ From elpi.apps Require Import derive.std.
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype fintype ssralg.
 From mathcomp Require Import word_ssrZ.
 
-Require Import
+From lang Require Import
   expr
   flag_combination
   sem_type
@@ -11,7 +11,7 @@ Require Import
   utils
   wsize.
 
-Require Import
+From arch Require Import
   arch_decl
   arch_utils.
 
diff --git a/proofs/compiler/riscv_extra.v b/proofs/compiler/riscv/riscv_extra.v
similarity index 84%
rename from proofs/compiler/riscv_extra.v
rename to proofs/compiler/riscv/riscv_extra.v
index 9a6c0f73d0..686b691435 100644
--- a/proofs/compiler/riscv_extra.v
+++ b/proofs/compiler/riscv/riscv_extra.v
@@ -2,20 +2,21 @@ From elpi.apps Require Import derive.std.
 From HB Require Import structures.
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssralg.
 
-Require Import
-  compiler_util
+From lang Require Import
   expr
   fexpr
   sopn
   utils.
-Require Export
+From compiler Require Import
+  compiler_util.
+From arch Require Export
   arch_decl
-  arch_extra
-  riscv_params_core.
+  arch_extra.
 Require Import
   riscv_decl
   riscv_instr_decl
-  riscv.
+  riscv
+  riscv_params_core.
 
 Local Notation E n := (sopn.ADExplicit n sopn.ACR_any).
 
@@ -105,7 +106,7 @@ Definition assemble_extra
            (o: riscv_extra_op)
            (outx: lexprs)
            (inx: rexprs)
-           : cexec (seq (asm_op_msb_t * lexprs * rexprs)) :=
+           : result (bool * string) (seq (asm_op_msb_t * lexprs * rexprs)) :=
   match o with   
   | SWAP sz =>
     if (sz == U32)%CMP then
@@ -113,11 +114,11 @@ Definition assemble_extra
       | [:: LLvar x; LLvar y], [:: Rexpr (Fvar z); Rexpr (Fvar w)] =>
         (* x, y = swap(z, w) *)
         Let _ := assert (v_var x != v_var w)
-          (E.internal_error ii "bad RISC-V swap : x = w") in
+          (true, "bad RISC-V swap : x = w"%string) in
         Let _ := assert (v_var y != v_var x)
-          (E.internal_error ii "bad RISC-V swap : y = x") in
+          (true, "bad RISC-V swap : y = x"%string) in
         Let _ := assert (all (fun (x:var_i) => vtype x == sword U32) [:: x; y; z; w])
-          (E.error ii "RISC-V swap only valid for register of type u32") in
+          (false, "RISC-V swap only valid for register of type u32"%string) in
 
         ok [:: ((None, XOR), [:: LLvar x], [:: Rexpr (Fvar z); Rexpr (Fvar w)]);
                (* x = z ^ w *)
@@ -125,20 +126,20 @@ Definition assemble_extra
                (* y = x ^ w = z ^ w ^ w = z *)
                ((None, XOR), [:: LLvar x], [:: Rexpr (Fvar x); Rexpr (Fvar y)])
            ]   (* x = x ^ y = z ^ w ^ z = w *)
-      | _, _ => Error (E.error ii "only register is accepted on source and destination of the swap instruction on RISC-V")
+      | _, _ => Error (false, "only register is accepted on source and destination of the swap instruction on RISC-V"%string)
       end
     else
-      Error (E.error ii "RISC-V swap only valid for register of type u32")
+      Error (false, "RISC-V swap only valid for register of type u32"%string)
   | Oriscv_add_large_imm =>
     match outx, inx with
     | [:: LLvar x], [:: Rexpr (Fvar y); Rexpr (Fapp1 (Oword_of_int ws) (Fconst imm))] =>
       Let _ := assert (v_var x != v_var y)
-         (E.internal_error ii "bad riscv_add_large_imm: invalid register") in
+         (true, "bad riscv_add_large_imm: invalid register"%string) in
       Let _ := assert (all (fun (x:var_i) => vtype x == sword U32) [:: x; y])
-          (E.error ii "riscv_add_large_imm only valid for register of type u32") in
+          (false, "riscv_add_large_imm only valid for register of type u32"%string) in
       ok (asm_args_of_opn_args (RISCVFopn_core.smart_addi x y imm))
     | _, _ =>
-      Error (E.internal_error ii "bad riscv_add_large_imm: invalid args or dests")
+      Error (true, "bad riscv_add_large_imm: invalid args or dests"%string)
     end   
   end.
 
diff --git a/proofs/compiler/riscv_instr_decl.v b/proofs/compiler/riscv/riscv_instr_decl.v
similarity index 99%
rename from proofs/compiler/riscv_instr_decl.v
rename to proofs/compiler/riscv/riscv_instr_decl.v
index f063132138..eed40e7e5b 100644
--- a/proofs/compiler/riscv_instr_decl.v
+++ b/proofs/compiler/riscv/riscv_instr_decl.v
@@ -4,15 +4,15 @@ From elpi.apps Require Import derive.std.
 From mathcomp Require Import ssreflect ssrfun ssrbool seq eqtype ssralg.
 From mathcomp Require Import word_ssrZ.
 
-Require Import
+From thirdparty Require xseq.
+From lang Require Import
   sem_type
   shift_kind
   strings
   utils
-  word.
-Require xseq.
-Require Import
-  sopn
+  word
+  sopn.
+From arch Require Import
   arch_decl
   arch_utils.
 Require Import riscv_decl.
diff --git a/proofs/compiler/riscv_lower_addressing.v b/proofs/compiler/riscv/riscv_lower_addressing.v
similarity index 96%
rename from proofs/compiler/riscv_lower_addressing.v
rename to proofs/compiler/riscv/riscv_lower_addressing.v
index 9294688632..5d7fec0b4b 100644
--- a/proofs/compiler/riscv_lower_addressing.v
+++ b/proofs/compiler/riscv/riscv_lower_addressing.v
@@ -2,14 +2,20 @@ From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssralg.
 From mathcomp Require Import word_ssrZ.
 From Coq Require Import ZArith.
 
-Require Import expr sem_op_typed compiler_util lea.
+From lang Require Import
+  expr
+  sem_op_typed.
+From compiler Require Import
+  compiler_util
+  lea.
 
 Import Utf8.
 Import oseq.
 
-Require Import
+From arch Require Import
   arch_decl
-  arch_extra
+  arch_extra.
+Require Import
   riscv_instr_decl
   riscv_decl
   riscv
diff --git a/proofs/compiler/riscv_lower_addressing_proof.v b/proofs/compiler/riscv/riscv_lower_addressing_proof.v
similarity index 99%
rename from proofs/compiler/riscv_lower_addressing_proof.v
rename to proofs/compiler/riscv/riscv_lower_addressing_proof.v
index 0ddeaa834b..85ea8f1606 100644
--- a/proofs/compiler/riscv_lower_addressing_proof.v
+++ b/proofs/compiler/riscv/riscv_lower_addressing_proof.v
@@ -2,12 +2,18 @@
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype.
 From mathcomp Require Import ssralg.
 
-Require Import psem psem_facts compiler_util lea_proof.
-
-Require Import
+From lang Require Import
+  psem
+  psem_facts.
+From compiler Require Import
+  compiler_util
+  lea_proof.
+
+From arch Require Import
   arch_decl
   arch_extra
-  sem_params_of_arch_extra
+  sem_params_of_arch_extra.
+Require Import
   riscv_instr_decl
   riscv_decl
   riscv
diff --git a/proofs/compiler/riscv_lowering.v b/proofs/compiler/riscv/riscv_lowering.v
similarity index 98%
rename from proofs/compiler/riscv_lowering.v
rename to proofs/compiler/riscv/riscv_lowering.v
index 2d829eb240..da50259272 100644
--- a/proofs/compiler/riscv_lowering.v
+++ b/proofs/compiler/riscv/riscv_lowering.v
@@ -1,13 +1,14 @@
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssralg.
 From mathcomp Require Import word_ssrZ.
 
-Require Import
-  compiler_util
+From lang Require Import
   expr
-  lowering
   pseudo_operator
   shift_kind.
-Require Import
+From compiler Require Import
+  compiler_util
+  lowering.
+From arch Require Import
   arch_decl
   arch_extra.
 Require Import
diff --git a/proofs/compiler/riscv_lowering_proof.v b/proofs/compiler/riscv/riscv_lowering_proof.v
similarity index 99%
rename from proofs/compiler/riscv_lowering_proof.v
rename to proofs/compiler/riscv/riscv_lowering_proof.v
index aebdaad87c..c5419c9c89 100644
--- a/proofs/compiler/riscv_lowering_proof.v
+++ b/proofs/compiler/riscv/riscv_lowering_proof.v
@@ -6,14 +6,15 @@ From mathcomp Require Import word_ssrZ.
 
 From Coq Require Import Lia.
 
-Require Import
-  compiler_util
+From lang Require Import
   expr
-  lowering
-  lowering_lemmas
   psem
   utils.
-Require Import
+From compiler Require Import
+  compiler_util
+  lowering
+  lowering_lemmas.
+From arch Require Import
   arch_extra
   sem_params_of_arch_extra.
 Require Import
diff --git a/proofs/compiler/riscv_params.v b/proofs/compiler/riscv/riscv_params.v
similarity index 98%
rename from proofs/compiler/riscv_params.v
rename to proofs/compiler/riscv/riscv_params.v
index 26219cd47e..59096aa479 100644
--- a/proofs/compiler/riscv_params.v
+++ b/proofs/compiler/riscv/riscv_params.v
@@ -1,22 +1,22 @@
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype.
 From mathcomp Require Import word_ssrZ.
 
-Require Import
-  arch_params
-  compiler_util
+From lang Require Import
   expr
   fexpr.
-Require Import
+From compiler Require Import
+  arch_params
+  asm_gen
+  compiler_util
   lea
   linearization
   lowering
   stack_alloc_params
   stack_zeroization
   slh_lowering.
-Require Import
+From arch Require Import
   arch_decl
-  arch_extra
-  asm_gen.
+  arch_extra.
 
 Require Import
   riscv_decl
diff --git a/proofs/compiler/riscv_params_common.v b/proofs/compiler/riscv/riscv_params_common.v
similarity index 95%
rename from proofs/compiler/riscv_params_common.v
rename to proofs/compiler/riscv/riscv_params_common.v
index 4f4f57f0ec..fc3062a122 100644
--- a/proofs/compiler/riscv_params_common.v
+++ b/proofs/compiler/riscv/riscv_params_common.v
@@ -1,13 +1,14 @@
 From mathcomp Require Import ssreflect ssrfun ssrbool.
 From mathcomp Require Import word_ssrZ.
 
-Require Import
-  arch_params
-  compiler_util
+From lang Require Import
   expr
   fexpr
   linear.
-Require Import
+From compiler Require Import
+  arch_params
+  compiler_util.
+From arch Require Import
   arch_decl
   arch_extra.
 Require Import
diff --git a/proofs/compiler/riscv_params_common_proof.v b/proofs/compiler/riscv/riscv_params_common_proof.v
similarity index 99%
rename from proofs/compiler/riscv_params_common_proof.v
rename to proofs/compiler/riscv/riscv_params_common_proof.v
index 485919a07e..90927535fa 100644
--- a/proofs/compiler/riscv_params_common_proof.v
+++ b/proofs/compiler/riscv/riscv_params_common_proof.v
@@ -3,9 +3,7 @@ From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat ssralg.
 
 From mathcomp Require Import word_ssrZ.
 
-Require Import
-  arch_params
-  compiler_util
+From lang Require Import
   expr
   fexpr
   fexpr_sem
@@ -13,7 +11,10 @@ Require Import
   linear_sem
   linear_facts
   psem.
-Require Import
+From compiler Require Import
+  arch_params
+  compiler_util.
+From arch Require Import
   arch_decl
   arch_extra
   sem_params_of_arch_extra.
diff --git a/proofs/compiler/riscv_params_core.v b/proofs/compiler/riscv/riscv_params_core.v
similarity index 96%
rename from proofs/compiler/riscv_params_core.v
rename to proofs/compiler/riscv/riscv_params_core.v
index 52ab4c624b..c3079c9a31 100644
--- a/proofs/compiler/riscv_params_core.v
+++ b/proofs/compiler/riscv/riscv_params_core.v
@@ -1,12 +1,13 @@
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype.
 From mathcomp Require Import word_ssrZ.
 
-Require Import
-  compiler_util
+From lang Require Import
   expr
   fexpr
   linear.
-Require Import
+From compiler Require Import
+  compiler_util.
+From arch Require Import
   arch_decl.
 Require Import
   riscv_decl
diff --git a/proofs/compiler/riscv_params_core_proof.v b/proofs/compiler/riscv/riscv_params_core_proof.v
similarity index 99%
rename from proofs/compiler/riscv_params_core_proof.v
rename to proofs/compiler/riscv/riscv_params_core_proof.v
index 8cabd5e3f2..50af7ec205 100644
--- a/proofs/compiler/riscv_params_core_proof.v
+++ b/proofs/compiler/riscv/riscv_params_core_proof.v
@@ -2,9 +2,7 @@ From Coq Require Import Lia.
 From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat eqtype ssralg.
 From mathcomp Require Import word_ssrZ.
 
-Require Import
-  arch_params
-  compiler_util
+From lang Require Import
   expr
   fexpr
   fexpr_sem
@@ -12,7 +10,10 @@ Require Import
   linear_sem
   linear_facts
   psem.
-Require Import
+From compiler Require Import
+  arch_params
+  compiler_util.
+From arch Require Import
   arch_decl
   arch_sem.
 
diff --git a/proofs/compiler/riscv_params_proof.v b/proofs/compiler/riscv/riscv_params_proof.v
similarity index 99%
rename from proofs/compiler/riscv_params_proof.v
rename to proofs/compiler/riscv/riscv_params_proof.v
index 0ff7930f54..dcc21614d3 100644
--- a/proofs/compiler/riscv_params_proof.v
+++ b/proofs/compiler/riscv/riscv_params_proof.v
@@ -2,31 +2,33 @@ From Coq Require Import Relations.
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssralg.
 From mathcomp Require Import word_ssrZ.
 
-Require Import oseq.
+From ssrmisc Require Import oseq.
 
-Require Import
-  arch_params_proof
-  compiler_util
+From lang Require Import
   expr
   fexpr
   fexpr_sem
   psem
   psem_facts
-  sem_one_varmap.
-Require Import
+  sem_one_varmap
+  linear_sem
+  linear_facts.
+From compiler Require Import
+  arch_params_proof
+  asm_gen
+  asm_gen_proof
+  compiler_util
   lea_proof
   linearization
   linearization_proof
   lowering
   stack_alloc_params_proof
   stack_zeroization_proof.
-Require
+From arch Require
   arch_sem.
-Require Import
+From arch Require Import
   arch_decl
   arch_extra
-  asm_gen
-  asm_gen_proof
   sem_params_of_arch_extra.
 Require Import
   riscv_decl
@@ -500,7 +502,7 @@ Proof.
     have hincl := hind _ ok_c _ ok_v.
     by have [_ [<-] ?] := eval_assemble_cond_Onot erefl hincl ok_v1.
 
-  t_xrbindP=> c [ck b] /o2rP hop2.
+  t_xrbindP=> c [ck b] hop2.
   t_xrbindP=> arg1 ok_arg1 arg2 ok_arg2 ok_c v v1 ok_v1 v2 ok_v2 ok_v.
   have hincl1 := assemble_cond_argP eqr ok_arg1 ok_v1.
   have hincl2 := assemble_cond_argP eqr ok_arg2 ok_v2.
diff --git a/proofs/compiler/riscv_stack_zeroization.v b/proofs/compiler/riscv/riscv_stack_zeroization.v
similarity index 96%
rename from proofs/compiler/riscv_stack_zeroization.v
rename to proofs/compiler/riscv/riscv_stack_zeroization.v
index 6bb02a35c6..db5dc47a5e 100644
--- a/proofs/compiler/riscv_stack_zeroization.v
+++ b/proofs/compiler/riscv/riscv_stack_zeroization.v
@@ -1,16 +1,19 @@
-Require Import
+From lang Require Import
   expr
   fexpr
   label
   linear
-  stack_zero_strategy
+  stack_zero_strategy.
+From arch Require Import
   arch_decl
-  arch_extra
+  arch_extra.
+From compiler Require Import
+  compiler_util.
+Require Import
   riscv_decl
   riscv_extra
   riscv_instr_decl
   riscv_params_common.
-Require Import compiler_util.
 
 Section STACK_ZEROIZATION.
 
diff --git a/proofs/compiler/riscv_stack_zeroization_proof.v b/proofs/compiler/riscv/riscv_stack_zeroization_proof.v
similarity index 99%
rename from proofs/compiler/riscv_stack_zeroization_proof.v
rename to proofs/compiler/riscv/riscv_stack_zeroization_proof.v
index 5a61c22281..96f4718cb0 100644
--- a/proofs/compiler/riscv_stack_zeroization_proof.v
+++ b/proofs/compiler/riscv/riscv_stack_zeroization_proof.v
@@ -2,7 +2,7 @@ From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat eqtype ssralg.
 From mathcomp Require Import word_ssrZ.
 From Coq Require Import Lia.
 
-Require Import
+From lang Require Import
   expr
   fexpr
   fexpr_sem
@@ -12,11 +12,11 @@ Require Import
   psem
   psem_facts
   low_memory.
-Require stack_zeroization_proof.
-Require Import
+From arch Require Import
   arch_decl
   arch_extra
   sem_params_of_arch_extra.
+From compiler Require stack_zeroization_proof.
 Require Import
   riscv_decl
   riscv_extra
diff --git a/proofs/compiler/slh_lowering.v b/proofs/compiler/slh_lowering.v
index a8a4839329..c494bb35e6 100644
--- a/proofs/compiler/slh_lowering.v
+++ b/proofs/compiler/slh_lowering.v
@@ -20,8 +20,8 @@
 
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype.
 
-Require Import expr.
-Require constant_prop flag_combination.
+From lang Require Import expr flag_combination.
+Require constant_prop.
 Require Import compiler_util.
 
 Module E.
diff --git a/proofs/compiler/slh_lowering_proof.v b/proofs/compiler/slh_lowering_proof.v
index 25cdfe4b80..c8e169d6b0 100644
--- a/proofs/compiler/slh_lowering_proof.v
+++ b/proofs/compiler/slh_lowering_proof.v
@@ -1,14 +1,15 @@
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssralg.
 
-Require Import
+From lang Require Import
   expr
   psem.
 Require Import
   compiler_util
   slh_lowering.
-Require Import psem_facts.
+From lang Require Import psem_facts.
+From lang Require
+  expr_facts.
 Require
-  expr_facts
   constant_prop_proof.
 
 Section CONST_PROP.
diff --git a/proofs/compiler/stack_alloc.v b/proofs/compiler/stack_alloc.v
index 9d83a564ff..dffff7e97a 100644
--- a/proofs/compiler/stack_alloc.v
+++ b/proofs/compiler/stack_alloc.v
@@ -3,7 +3,7 @@ From elpi.apps Require Import derive.std.
 From HB Require Import structures.
 From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat seq eqtype ssralg.
 From mathcomp Require Import word_ssrZ.
-Require Import strings word utils type var expr.
+From lang Require Import strings word utils type var expr.
 Require Import compiler_util.
 Require slh_lowering.
 From Coq Require Import ZArith.
diff --git a/proofs/compiler/stack_alloc_params.v b/proofs/compiler/stack_alloc_params.v
index 7e61e63770..10ab363149 100644
--- a/proofs/compiler/stack_alloc_params.v
+++ b/proofs/compiler/stack_alloc_params.v
@@ -1,5 +1,5 @@
 From mathcomp Require Import ssreflect.
-Require Import expr.
+From lang Require Import expr.
 
 Section WITH_PARAMS.
 
diff --git a/proofs/compiler/stack_alloc_params_proof.v b/proofs/compiler/stack_alloc_params_proof.v
index a01b7da2dc..cdb8a48def 100644
--- a/proofs/compiler/stack_alloc_params_proof.v
+++ b/proofs/compiler/stack_alloc_params_proof.v
@@ -1,6 +1,6 @@
 From mathcomp Require Import ssreflect seq ssralg.
 From Coq Require Import Utf8.
-Require Import psem.
+From lang Require Import psem.
 Require Export stack_alloc_params.
 
 (* TODO : move elsewhere *)
diff --git a/proofs/compiler/stack_alloc_proof_1.v b/proofs/compiler/stack_alloc_proof_1.v
index d02a4425d0..056ef9acf9 100644
--- a/proofs/compiler/stack_alloc_proof_1.v
+++ b/proofs/compiler/stack_alloc_proof_1.v
@@ -2,7 +2,9 @@
 From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat seq eqtype fintype.
 From mathcomp Require Import div ssralg.
 From mathcomp Require Import word_ssrZ.
-Require Import seq_extra psem psem_facts compiler_util low_memory.
+From ssrmisc Require Import seq_extra.
+From lang Require Import psem psem_facts low_memory.
+Require Import compiler_util.
 Require Export stack_alloc stack_alloc_params_proof.
 Require slh_lowering_proof.
 Import Utf8 Lia.
diff --git a/proofs/compiler/stack_alloc_proof_2.v b/proofs/compiler/stack_alloc_proof_2.v
index f807d9157a..b11f1a2e20 100644
--- a/proofs/compiler/stack_alloc_proof_2.v
+++ b/proofs/compiler/stack_alloc_proof_2.v
@@ -7,7 +7,8 @@ From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat seq eqtype.
 From mathcomp Require Import ssralg.
 From mathcomp Require Import word_ssrZ.
 Require Import Uint63.
-Require Import psem psem_facts compiler_util.
+From lang Require Import psem psem_facts.
+Require Import compiler_util.
 Require Export stack_alloc stack_alloc_proof_1.
 From mathcomp Require Import ring.
 From Coq Require Import Utf8 Lia.
diff --git a/proofs/compiler/stack_zeroization.v b/proofs/compiler/stack_zeroization.v
index a6662b407c..b86a70255e 100644
--- a/proofs/compiler/stack_zeroization.v
+++ b/proofs/compiler/stack_zeroization.v
@@ -16,17 +16,17 @@ From mathcomp Require Import ssreflect ssrfun ssrbool.
 From mathcomp Require Import word_ssrZ.
 From Coq Require Import ZArith.
 
-Require Import
+From lang Require Import
   expr
   label
   linear
+  one_varmap
   sopn
   utils
   word
   wsize.
 Require Import compiler_util linear_util.
-Require Import one_varmap.
-Require Export stack_zero_strategy.
+From lang Require Export stack_zero_strategy.
 
 Module E.
 
diff --git a/proofs/compiler/stack_zeroization_proof.v b/proofs/compiler/stack_zeroization_proof.v
index 368bb6b47a..30166fd475 100644
--- a/proofs/compiler/stack_zeroization_proof.v
+++ b/proofs/compiler/stack_zeroization_proof.v
@@ -2,15 +2,15 @@ From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssralg.
 From mathcomp Require Import word_ssrZ.
 From Coq Require Import ZArith.
 
-Require Import
+From lang Require Import
   label
   psem
   one_varmap
   linear
-  linear_util
   linear_sem
   linear_facts.
-Require Import seq_extra compiler_util.
+From ssrmisc Require Import seq_extra.
+Require Import compiler_util linear_util.
 Require Export stack_zeroization.
 
 Section WITH_PARAMS.
diff --git a/proofs/compiler/tunneling.v b/proofs/compiler/tunneling.v
index 59590a1b96..6b85549c25 100644
--- a/proofs/compiler/tunneling.v
+++ b/proofs/compiler/tunneling.v
@@ -2,8 +2,10 @@ From mathcomp Require Import ssreflect ssrfun ssrbool eqtype.
 From Coq Require Import ZArith.
 
 From Coq Require Import Utf8.
-Require Import expr compiler_util linear label.
-Require Import seq_extra unionfind.
+From lang Require Import expr linear label.
+Require Import compiler_util.
+From ssrmisc Require Import seq_extra.
+Require Import unionfind.
 
 
 
diff --git a/proofs/compiler/tunneling_proof.v b/proofs/compiler/tunneling_proof.v
index 58e63899b7..da6618f63a 100644
--- a/proofs/compiler/tunneling_proof.v
+++ b/proofs/compiler/tunneling_proof.v
@@ -2,15 +2,14 @@ From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat eqtype.
 From Coq Require Import ZArith.
 From Coq Require Import Utf8.
 
-Require Import expr_facts compiler_util label linear linear_sem.
-Require Import sem_params.
+From lang Require Import expr_facts label linear linear_sem sem_params.
+Require Import compiler_util.
 Import word_ssrZ.
 
 Local Open Scope seq_scope.
 
-Require Import oseq seq_extra unionfind tunneling unionfind_proof.
-Require Import linear_sem.
-
+From ssrmisc Require Import oseq seq_extra.
+Require Import unionfind tunneling unionfind_proof.
 
 
 Section WITH_PARAMS.
diff --git a/proofs/compiler/unionfind.v b/proofs/compiler/unionfind.v
index 7605efebfc..cb63136904 100644
--- a/proofs/compiler/unionfind.v
+++ b/proofs/compiler/unionfind.v
@@ -1,6 +1,6 @@
 From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat eqtype.
 From Coq Require Import Utf8.
-Require Import expr label.
+From lang Require Import expr label.
 
 
 Module Type EqType.
diff --git a/proofs/compiler/unionfind_proof.v b/proofs/compiler/unionfind_proof.v
index e44e02fe87..3f18b48ff2 100644
--- a/proofs/compiler/unionfind_proof.v
+++ b/proofs/compiler/unionfind_proof.v
@@ -1,6 +1,6 @@
 From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat eqtype.
 From Coq Require Import Utf8.
-Require Import expr label.
+From lang Require Import expr label.
 
 Require Import unionfind.
 
diff --git a/proofs/compiler/unrolling.v b/proofs/compiler/unrolling.v
index 6dc4fe5155..e6a1376502 100644
--- a/proofs/compiler/unrolling.v
+++ b/proofs/compiler/unrolling.v
@@ -2,7 +2,8 @@
 
 From mathcomp Require Import ssreflect ssrfun ssrbool.
 From Coq Require Import ZArith.
-Require Import expr compiler_util.
+From lang Require Import expr.
+Require Import compiler_util.
 
 Local Open Scope seq_scope.
 
diff --git a/proofs/compiler/unrolling_proof.v b/proofs/compiler/unrolling_proof.v
index 1bee48645f..c1e179929b 100644
--- a/proofs/compiler/unrolling_proof.v
+++ b/proofs/compiler/unrolling_proof.v
@@ -1,7 +1,8 @@
 (* ** Imports and settings *)
 From mathcomp Require Import ssreflect ssrfun ssrbool.
 From Coq Require Import ZArith.
-Require Import psem compiler_util.
+From lang Require Import psem.
+Require Import compiler_util.
 Require Export unrolling.
 
 Local Open Scope seq_scope.
diff --git a/proofs/compiler/wint_int.v b/proofs/compiler/wint_int.v
index 4b4f9309d0..cb45732513 100644
--- a/proofs/compiler/wint_int.v
+++ b/proofs/compiler/wint_int.v
@@ -3,10 +3,10 @@ From HB Require Import structures.
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssralg.
 From mathcomp Require Import word_ssrZ.
 From Coq Require Import ZArith.
-Require Import expr sem_op_typed compiler_util.
+From lang Require Import expr sem_op_typed flag_combination.
+Require Import compiler_util.
 Import Utf8.
 Import oseq.
-Require Import flag_combination.
 
 Local Open Scope seq_scope.
 Local Open Scope Z_scope.
diff --git a/proofs/compiler/wint_int_proof.v b/proofs/compiler/wint_int_proof.v
index 3118c2a0e6..75698eccb3 100644
--- a/proofs/compiler/wint_int_proof.v
+++ b/proofs/compiler/wint_int_proof.v
@@ -1,4 +1,5 @@
-Require Import compiler_util psem psem_facts.
+From lang Require Import psem psem_facts.
+Require Import compiler_util.
 Require Import wint_int.
 Import Utf8.
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssralg.
@@ -617,7 +618,7 @@ Qed.
 
 Local Lemma HmkI : sem_Ind_mkI p ev Pi_r Pi.
 Proof.
-  move=> i_i i s1 s2 _ hi ? /=; t_xrbindP => ii /add_iinfoP /hi{}hi <- si /hi [si' ??].
+  move=> i_i i s1 s2 _ hi ? /=; t_xrbindP => ii /hi{}hi <- si /hi [si' ??].
   exists si' => //; constructor.
 Qed.
 
diff --git a/proofs/compiler/wint_word.v b/proofs/compiler/wint_word.v
index 854c6b6ec2..b6f926509a 100644
--- a/proofs/compiler/wint_word.v
+++ b/proofs/compiler/wint_word.v
@@ -3,10 +3,10 @@ From HB Require Import structures.
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssralg.
 From mathcomp Require Import word_ssrZ.
 From Coq Require Import ZArith.
-Require Import expr sem_op_typed compiler_util allocation.
+From lang Require Import expr sem_op_typed flag_combination.
+Require Import compiler_util allocation.
 Import Utf8.
 Import oseq.
-Require Import flag_combination.
 
 Local Open Scope seq_scope.
 Local Open Scope Z_scope.
diff --git a/proofs/compiler/wint_word_proof.v b/proofs/compiler/wint_word_proof.v
index efa2464eb7..44f2c92bb4 100644
--- a/proofs/compiler/wint_word_proof.v
+++ b/proofs/compiler/wint_word_proof.v
@@ -1,4 +1,5 @@
-Require Import compiler_util psem psem_facts.
+From lang Require Import psem psem_facts.
+Require Import compiler_util.
 Require Import wint_word allocation_proof.
 Import Utf8.
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssralg.
diff --git a/proofs/compiler/x86/_CoqProject b/proofs/compiler/x86/_CoqProject
new file mode 100644
index 0000000000..7dcda800c5
--- /dev/null
+++ b/proofs/compiler/x86/_CoqProject
@@ -0,0 +1,25 @@
+-R ../../_build/default/arch arch
+-R ../../_build/default/compiler compiler
+-R ../../_build/default/common common
+-R ../../_build/default/lang lang
+-R ../../_build/default/itrees itrees
+-R ../../_build/default/ssrmisc ssrmisc
+-R ../../_build/default/thirdparty thirdparty
+
+-R ../../_build/default/compiler/x86 x86
+
+-arg "-set" -arg "'Uniform Inductive Parameters'"
+-arg "-set" -arg "'Implicit Arguments'"
+-arg "-unset" -arg "'Strict Implicit'"
+-arg "-unset" -arg "'Printing Implicit Defensive'"
+-arg "-w -notation-overridden"
+-arg "-w -extraction-reserved-identifier"
+-arg "-w -extraction-opaque-accessed"
+-arg "-w -ambiguous-paths"
+-arg "-w -redundant-canonical-projection"
+-arg "-w -projection-no-head-constant"
+-arg "-w -postfix-notation-not-level-1"
+-arg "-w -deprecated-since-mathcomp-2.3.0"
+-arg "-w -deprecated-since-mathcomp-2.4.0"
+-arg "-w -deprecated-from-Coq"
+-arg "-w -deprecated-dirpath-Coq"
diff --git a/proofs/compiler/x86/dune b/proofs/compiler/x86/dune
new file mode 100644
index 0000000000..c784a27899
--- /dev/null
+++ b/proofs/compiler/x86/dune
@@ -0,0 +1,3 @@
+(coq.theory
+  (name x86)
+  (theories ssrmisc thirdparty lang arch compiler))
diff --git a/proofs/compiler/x86.v b/proofs/compiler/x86/x86.v
similarity index 91%
rename from proofs/compiler/x86.v
rename to proofs/compiler/x86/x86.v
index 9cb6d323f3..17021ca2de 100644
--- a/proofs/compiler/x86.v
+++ b/proofs/compiler/x86/x86.v
@@ -1,5 +1,9 @@
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype.
-Require Import sem_type arch_decl x86_decl x86_instr_decl.
+From lang Require Import
+  sem_type.
+From arch Require Import
+  arch_decl.
+Require Import x86_decl x86_instr_decl.
 
 Definition x86_eval_cond (get : rflag -> result error bool) (c : condt) :=
   match c with
diff --git a/proofs/compiler/x86_decl.v b/proofs/compiler/x86/x86_decl.v
similarity index 98%
rename from proofs/compiler/x86_decl.v
rename to proofs/compiler/x86/x86_decl.v
index 75f4150e80..eba6f40f8d 100644
--- a/proofs/compiler/x86_decl.v
+++ b/proofs/compiler/x86/x86_decl.v
@@ -2,18 +2,18 @@ From elpi.apps Require Import derive.std.
 From HB Require Import structures.
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype choice fintype.
 From mathcomp Require Import word_ssrZ.
-Require oseq.
 From Coq Require Import ZArith Utf8 Relation_Operators.
-Require Import
+From ssrmisc Require Import oseq.
+From lang Require Import
   utils
-  strings wsize
+  strings
+  wsize
   memory_model
   (* word *)
   global
-  oseq
-  sem_type.
-Require Import flag_combination.
-Require Import
+  sem_type
+  flag_combination.
+From arch Require Import
   arch_decl
   arch_utils.
 
diff --git a/proofs/compiler/x86_extra.v b/proofs/compiler/x86/x86_extra.v
similarity index 84%
rename from proofs/compiler/x86_extra.v
rename to proofs/compiler/x86/x86_extra.v
index 5c8dd4cd0a..15fe234aa7 100644
--- a/proofs/compiler/x86_extra.v
+++ b/proofs/compiler/x86/x86_extra.v
@@ -4,43 +4,33 @@ From HB Require Import structures.
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssralg.
 From mathcomp Require Import word_ssrZ.
 From Coq Require Import Utf8.
-Require Import compiler_util.
-Require Import
-  arch_decl
+From lang Require Import
   expr
   fexpr
-  wsize
-  asm_gen.
+  wsize.
+From arch Require Import
+  arch_decl.
+From arch Require Export
+  arch_extra.
+From compiler Require Import
+  compiler_util.
 Require Import
   x86_decl
   x86_instr_decl
   x86.
-Require Export arch_extra.
 Import sopn.
+Import wsize.
 
 Module E.
 
-Definition pass_name := "asmgen"%string.
-
-Definition error (ii : instr_info) (msg : string) :=
-  {|
-    pel_msg := compiler_util.pp_s msg;
-    pel_fn := None;
-    pel_fi := None;
-    pel_ii := Some ii;
-    pel_vi := None;
-    pel_pass := Some pass_name;
-    pel_internal := true;
-  |}.
-
-Definition se_update_arguments (ii : instr_info) : pp_error_loc :=
-  compiler_util.pp_internal_error_s_at pass_name ii "x86_update_msf arguments are invalid.".
+Definition se_update_arguments :=
+  (true, "x86_update_msf arguments are invalid."%string).
 
-Definition se_protect_arguments (ii : instr_info) : pp_error_loc :=
-  compiler_util.pp_internal_error_s_at pass_name ii "x86_protect arguments are invalid.".
+Definition se_protect_arguments :=
+  (true, "x86_protect arguments are invalid."%string).
 
-Definition se_protect_ptr (ii : instr_info) : pp_error_loc :=
-  compiler_util.pp_internal_error_s_at pass_name ii "Found protect_ptr.".
+Definition se_protect_ptr :=
+  (true, "Found protect_ptr."%string).
 
 End E.
 
@@ -225,7 +215,7 @@ Definition re8_1 := re_i U8 1.
 #[local] Notation "x ::= o e" := ((None, o), x, e) (at level 70, no associativity, o at level 0, only parsing).
 
 Definition assemble_slh_init
-  (les : seq lexpr) : cexec (seq (asm_op_msb_t * seq lexpr * seq rexpr)) :=
+  (les : seq lexpr) : result (bool * string) (seq (asm_op_msb_t * seq lexpr * seq rexpr)) :=
   ok
     [:: [::] ::= LFENCE [::];
         les  ::= (MOV U64) [:: re_i U64 0 ]
@@ -235,12 +225,12 @@ Definition assemble_slh_update
   (ii : instr_info)
   (les : seq lexpr)
   (res : seq rexpr) :
-  cexec (seq (asm_op_msb_t * seq lexpr * seq rexpr)) :=
+  result (bool * string) (seq (asm_op_msb_t * seq lexpr * seq rexpr)) :=
   if (les, res) is ([:: LLvar aux; ms0 ], [:: Rexpr b; msf ])
   then
     Let _ := assert (~~(Sv.mem aux (free_vars b) || Sv.mem aux (free_vars_r msf)) &&
                      (vtype aux == sword U64))
-                    (E.se_update_arguments ii) in
+                    (E.se_update_arguments) in
     let res' := [:: Rexpr (Fapp1 Onot b); Rexpr (Fvar aux); msf ] in
     ok
       [::
@@ -248,7 +238,7 @@ Definition assemble_slh_update
                [:: ms0 ] ::= (CMOVcc U64) res'
       ]
   else
-    Error (E.se_update_arguments ii).
+    Error (E.se_update_arguments).
 
 Definition assemble_slh_protect
   (ii : instr_info)
@@ -256,7 +246,7 @@ Definition assemble_slh_protect
   (ws : wsize)
   (les : seq lexpr)
   (res : seq rexpr) :
-  cexec (seq (asm_op_msb_t * seq lexpr * seq rexpr)) :=
+  result (bool * string) (seq (asm_op_msb_t * seq lexpr * seq rexpr)) :=
   if (ws <= U64)%CMP then
     ok [:: les ::= (if rk is Extra then POR else OR ws) res ]
   else if (les, res) is ([:: LLvar aux; y], [:: x; msf ]) then
@@ -266,55 +256,55 @@ Definition assemble_slh_protect
         y   = VPOR x aux
       *)
       Let _ := assert (~~(Sv.mem aux (free_vars_r x) || Sv.mem aux (free_vars_r msf)))
-                      (E.se_protect_arguments ii) in
+                      (E.se_protect_arguments) in
       let eaux := Rexpr (Fvar aux) in
       let laux := [:: LLvar aux] in
       ok ([::                     laux ::= (VPINSR VE64) [:: eaux; msf; re8_0]       ;
                                   laux ::= (VPINSR VE64) [:: eaux; msf; re8_1]       ] ++
           (if ws == U256 then [:: laux ::= (VINSERTI128) [:: eaux; eaux; re8_1]] else [::]) ++
           [::                   [:: y] ::= (VPOR ws)     [:: x; eaux]])
-  else Error (E.se_protect_arguments ii).
+  else Error (E.se_protect_arguments).
 
 Definition assemble_slh_move
   (les : seq lexpr)
   (res : seq rexpr) :
-  cexec (seq (asm_op_msb_t * seq lexpr * seq rexpr)) :=
+  result (bool * string) (seq (asm_op_msb_t * seq lexpr * seq rexpr)) :=
   let lmmx := if les is [:: LLvar x ] then is_regx x else false in
   let rmmx := if res is [:: Rexpr (Fvar x) ] then is_regx x else false in
   let op := if lmmx || rmmx then MOVX else MOV in
   ok [:: les ::= (op Uptr) res ].
 
-Definition assemble_extra ii o outx inx : cexec (seq (asm_op_msb_t * lexprs * rexprs)) :=
+Definition assemble_extra ii o outx inx : result (bool * string) (seq (asm_op_msb_t * lexprs * rexprs)) :=
   match o with
   | Oset0 sz =>
     let op := if (sz <= U64)%CMP then (XOR sz) else (VPXOR sz) in
     Let x :=
       match rev outx with
       | LLvar x :: _ =>  ok (Rexpr (Fvar x))
-      | _ => Error (E.error ii "set0 : destination is not a register")
+      | _ => Error (true, "set0 : destination is not a register"%string)
       end in
     ok [:: outx ::= op [:: x; x ] ]
   | Ox86MOVZX32 =>
     Let _ :=
       match outx with
       | [:: LLvar _ ] =>  ok tt
-      | _ => Error (E.error ii "Ox86MOVZX32: destination is not a register")
+      | _ => Error (true, "Ox86MOVZX32: destination is not a register"%string)
       end in
     ok [:: outx ::= (MOV U32) inx ]
   | Oconcat128 =>
     Let inx :=
       match inx with
       | [:: h; Rexpr (Fvar _) as l] => ok [:: l; h; re8_1]
-      |  _ => Error (E.error ii "Oconcat: assert false")
+      |  _ => Error (true, "Oconcat: assert false"%string)
       end in
     ok [:: outx ::= VINSERTI128 inx ]
   | Ox86MULX sz =>
     Let outx :=
       match outx with
       | [:: LLvar hi as h; LLvar lo as l ] =>
-          Let _ := assert (v_var lo != v_var hi) (E.error ii "Ox86MULX: lo = hi") in
+          Let _ := assert (v_var lo != v_var hi) (false, "Ox86MULX: lo = hi"%string) in
           ok [:: l; h]
-      | _ => Error (E.error ii "Ox86MULX: assert false")
+      | _ => Error (true, "Ox86MULX: assert false"%string)
       end in
     ok [:: outx ::= (MULX_lo_hi sz) inx]
 
@@ -322,7 +312,7 @@ Definition assemble_extra ii o outx inx : cexec (seq (asm_op_msb_t * lexprs * re
     Let outx :=
       match outx with
       | [:: LLvar hi] => ok [::LLvar hi; LLvar hi]
-      | _ => Error (E.error ii "Ox86MULX_hi: assert false")
+      | _ => Error (true, "Ox86MULX_hi: assert false"%string)
       end in
     ok [:: outx ::= (MULX_lo_hi sz) inx]
 
diff --git a/proofs/compiler/x86_instr_decl.v b/proofs/compiler/x86/x86_instr_decl.v
similarity index 99%
rename from proofs/compiler/x86_instr_decl.v
rename to proofs/compiler/x86/x86_instr_decl.v
index fa77c96f77..550cfb1f14 100644
--- a/proofs/compiler/x86_instr_decl.v
+++ b/proofs/compiler/x86/x86_instr_decl.v
@@ -2,10 +2,11 @@ From elpi.apps Require Import derive.std.
 From HB Require Import structures.
 From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat eqtype tuple.
 From mathcomp Require Import ssralg word word_ssrZ.
-Require Import utils strings word waes sha256 sem_type global oseq sopn.
+From ssrmisc Require Import oseq.
+From lang Require Import utils strings word waes sha256 sem_type global sopn.
 Import Utf8 Relation_Operators ZArith.
 
-Require Export arch_decl.
+From arch Require Export arch_decl.
 Require Import x86_decl.
 
 (* -------------------------------------------------------------------- *)
diff --git a/proofs/compiler/x86_lowering.v b/proofs/compiler/x86/x86_lowering.v
similarity index 99%
rename from proofs/compiler/x86_lowering.v
rename to proofs/compiler/x86/x86_lowering.v
index 48d0aef166..1169370565 100644
--- a/proofs/compiler/x86_lowering.v
+++ b/proofs/compiler/x86/x86_lowering.v
@@ -1,12 +1,13 @@
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssralg.
 From mathcomp Require Import word_ssrZ.
 From Coq Require Import Utf8.
-Require Import
-  compiler_util
+From lang Require Import
   expr
-  lowering
-  lea
   pseudo_operator.
+From compiler Require Import
+  compiler_util
+  lowering
+  lea.
 Require Import x86_decl x86_instr_decl x86_extra.
 
 Section Section.
diff --git a/proofs/compiler/x86_lowering_proof.v b/proofs/compiler/x86/x86_lowering_proof.v
similarity index 99%
rename from proofs/compiler/x86_lowering_proof.v
rename to proofs/compiler/x86/x86_lowering_proof.v
index b0ba45d01d..057c3b625b 100644
--- a/proofs/compiler/x86_lowering_proof.v
+++ b/proofs/compiler/x86/x86_lowering_proof.v
@@ -5,13 +5,19 @@
 From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat eqtype order.
 From mathcomp Require Import ssralg ssrnum word_ssrZ.
 From Coq Require Import ZArith.
-Require Import psem compiler_util lea_proof x86_instr_decl x86_extra.
-Require Import
+From lang Require Import
+  psem.
+From compiler Require Import
+  compiler_util
+  lea_proof
   lowering
   lowering_lemmas.
-Require Import
+From arch Require Import
   arch_extra
   sem_params_of_arch_extra.
+Require Import
+  x86_instr_decl
+  x86_extra.
 Require Export x86_lowering.
 Import Utf8 Lia.
 Import Order.POrderTheory Order.TotalTheory.
diff --git a/proofs/compiler/x86_params.v b/proofs/compiler/x86/x86_params.v
similarity index 98%
rename from proofs/compiler/x86_params.v
rename to proofs/compiler/x86/x86_params.v
index f4356c424c..1918febe16 100644
--- a/proofs/compiler/x86_params.v
+++ b/proofs/compiler/x86/x86_params.v
@@ -1,21 +1,21 @@
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype.
 From mathcomp Require Import word_ssrZ.
 
-Require Import
-  arch_params
-  compiler_util
+From lang Require Import
   expr
   fexpr.
-Require Import
+From compiler Require Import
+  arch_params
+  asm_gen
+  compiler_util
   linearization
   lowering
   stack_alloc_params
   stack_zeroization
   slh_lowering.
-Require Import
+From arch Require Import
   arch_decl
-  arch_extra
-  asm_gen.
+  arch_extra.
 Require Import
   x86_decl
   x86_extra
diff --git a/proofs/compiler/x86_params_proof.v b/proofs/compiler/x86/x86_params_proof.v
similarity index 99%
rename from proofs/compiler/x86_params_proof.v
rename to proofs/compiler/x86/x86_params_proof.v
index 4a2d04f86f..0d75a45810 100644
--- a/proofs/compiler/x86_params_proof.v
+++ b/proofs/compiler/x86/x86_params_proof.v
@@ -1,9 +1,7 @@
 From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat seq eqtype finfun.
 From mathcomp Require Import ssralg word_ssrZ.
 
-Require Import
-  arch_params_proof
-  compiler_util
+From lang Require Import
   expr
   fexpr
   fexpr_sem
@@ -11,8 +9,14 @@ Require Import
   psem
   psem_facts
   one_varmap
-  sem_one_varmap.
-Require Import
+  sem_one_varmap
+  linear_sem
+  linear_facts.
+From compiler Require Import
+  arch_params_proof
+  asm_gen
+  asm_gen_proof
+  compiler_util
   linearization
   linearization_proof
   lowering
@@ -20,13 +24,11 @@ Require Import
   slh_lowering_proof
   stack_alloc_params_proof
   stack_zeroization_proof.
-Require
+From arch Require
   arch_sem.
-Require Import
+From arch Require Import
   arch_decl
   arch_extra
-  asm_gen
-  asm_gen_proof
   sem_params_of_arch_extra.
 Require Import
   x86_decl
diff --git a/proofs/compiler/x86_stack_zeroization.v b/proofs/compiler/x86/x86_stack_zeroization.v
similarity index 98%
rename from proofs/compiler/x86_stack_zeroization.v
rename to proofs/compiler/x86/x86_stack_zeroization.v
index 371ec37f8f..9e8c0c9030 100644
--- a/proofs/compiler/x86_stack_zeroization.v
+++ b/proofs/compiler/x86/x86_stack_zeroization.v
@@ -1,15 +1,18 @@
-Require Import
+From lang Require Import
   expr
   fexpr
   label
   linear
-  stack_zero_strategy
+  stack_zero_strategy.
+From arch Require Import
   arch_decl
-  arch_extra
+  arch_extra.
+From compiler Require Import
+  compiler_util.
+Require Import
   x86_decl
   x86_extra
   x86_instr_decl.
-Require Import compiler_util.
 
 Section STACK_ZEROIZATION.
 
diff --git a/proofs/compiler/x86_stack_zeroization_proof.v b/proofs/compiler/x86/x86_stack_zeroization_proof.v
similarity index 99%
rename from proofs/compiler/x86_stack_zeroization_proof.v
rename to proofs/compiler/x86/x86_stack_zeroization_proof.v
index d2746dce42..70d2d288b8 100644
--- a/proofs/compiler/x86_stack_zeroization_proof.v
+++ b/proofs/compiler/x86/x86_stack_zeroization_proof.v
@@ -2,7 +2,7 @@ From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat eqtype ssralg.
 From mathcomp Require Import word_ssrZ.
 From Coq Require Import Lia.
 
-Require Import
+From lang Require Import
   expr
   fexpr
   fexpr_sem
@@ -12,11 +12,13 @@ Require Import
   psem
   psem_facts
   low_memory.
-Require stack_zeroization_proof.
-Require Import
+From arch Require Import
   arch_decl
   arch_extra
   sem_params_of_arch_extra.
+From compiler Require stack_zeroization_proof.
+From compiler Require Import
+  asm_gen. (* to have ovm_i *)
 Require Import
   x86_decl
   x86_extra
diff --git a/proofs/dune b/proofs/dune
new file mode 100644
index 0000000000..88937a94d9
--- /dev/null
+++ b/proofs/dune
@@ -0,0 +1,15 @@
+(env
+  (_ (coq (flags :standard
+         -set "Uniform Inductive Parameters"
+         -set "Implicit Arguments"
+         -unset "Strict Implicit"
+         -unset "Printing Implicit Defensive"
+         -w -notation-overridden
+         -w -ambiguous-paths
+         -w -redundant-canonical-projection
+         -w -projection-no-head-constant
+         -w -postfix-notation-not-level-1
+         -w -deprecated-since-mathcomp-2.3.0
+         -w -deprecated-since-mathcomp-2.4.0
+         -w -deprecated-from-Coq
+         -w -deprecated-dirpath-Coq))))
diff --git a/proofs/dune-project b/proofs/dune-project
new file mode 100644
index 0000000000..f93dc9cf4a
--- /dev/null
+++ b/proofs/dune-project
@@ -0,0 +1,5 @@
+(lang dune 3.8)
+(using coq 0.8)
+(name jasmin-proofs)
+(license MIT)
+(authors "The Jasmin development team")
diff --git a/proofs/extraction/_CoqProject b/proofs/extraction/_CoqProject
new file mode 100644
index 0000000000..59f888123a
--- /dev/null
+++ b/proofs/extraction/_CoqProject
@@ -0,0 +1,27 @@
+-R ../_build/default/arch arch
+-R ../_build/default/common common
+-R ../_build/default/compiler compiler
+-R ../_build/default/compiler/armv7 armv7
+-R ../_build/default/compiler/riscv riscv
+-R ../_build/default/compiler/x86 x86
+-R ../_build/default/lang lang
+-R ../_build/default/itrees itrees
+-R ../_build/default/ssrmisc ssrmisc
+-R ../_build/default/thirdparty thirdparty
+-R ../_build/default/jasmin_compiler jasmin_compiler
+
+-arg "-set" -arg "'Uniform Inductive Parameters'"
+-arg "-set" -arg "'Implicit Arguments'"
+-arg "-unset" -arg "'Strict Implicit'"
+-arg "-unset" -arg "'Printing Implicit Defensive'"
+-arg "-w -notation-overridden"
+-arg "-w -extraction-reserved-identifier"
+-arg "-w -extraction-opaque-accessed"
+-arg "-w -ambiguous-paths"
+-arg "-w -redundant-canonical-projection"
+-arg "-w -projection-no-head-constant"
+-arg "-w -postfix-notation-not-level-1"
+-arg "-w -deprecated-since-mathcomp-2.3.0"
+-arg "-w -deprecated-since-mathcomp-2.4.0"
+-arg "-w -deprecated-from-Coq"
+-arg "-w -deprecated-dirpath-Coq"
diff --git a/proofs/extraction/dune b/proofs/extraction/dune
new file mode 100644
index 0000000000..5619523a89
--- /dev/null
+++ b/proofs/extraction/dune
@@ -0,0 +1,166 @@
+(coq.extraction
+  (prelude extraction)
+  (theories HB elpi elpi_elpi mathcomp arch common compiler jasmin_compiler lang ssrmisc thirdparty armv7 riscv x86) ; Jasmin?
+  (flags -w -extraction-reserved-identifier
+         -w -extraction-opaque-accessed)
+  (extracted_modules
+    allocation
+    arch_decl
+    arch_extra
+    arch_params
+    arch_utils
+    arm_decl
+    arm_expand_imm
+    arm_extra
+    arm_instr_decl
+    arm_lowering
+    arm
+    arm_params_common
+    arm_params_core
+    arm_params
+    arm_stack_zeroization
+    array_copy
+    array_expansion
+    array_init
+    Ascii
+    asm_gen
+    bigop
+    BinInt
+    BinNat
+    BinNums
+    BinPosDef
+    BinPos
+    Bool
+    choice
+    CMorphisms
+    compiler
+    compiler_util
+    constant_prop
+    CRelationClasses
+    Datatypes
+    dead_calls
+    dead_code
+    DecidableType
+    div
+    eqb_core_defs
+    eqbOK
+    EqdepFacts
+    eqtype
+    Equalities
+    expr
+    fexpr
+    finfun
+    fintype
+    flag_combination
+    FMapAVL
+    FMapFacts
+    FMapList
+    gen_map
+    global
+    ident
+    Init
+    inline
+    Int
+    label
+    lea
+    linearization
+    linear
+    linear_util
+    List0
+    load_constants_in_cond
+    lowering
+    lower_spill
+    low_memory
+    makeReferenceArguments
+    memory_example
+    memory_model
+    merge_varmaps
+    MSetDecide
+    MSetEqProperties
+    MSetFacts
+    MSetInterface
+    MSetProperties
+    Nat0
+    one_varmap
+    OrderedType
+    order
+    Orders
+    OrdersTac
+    oseq
+    param1
+    param1_trivial
+    PeanoNat
+    post_unrolling_check
+    Prelude
+    PrimInt63
+    propagate_inline
+    psem_defs
+    pseudo_operator
+    remove_globals
+    result
+    riscv_decl
+    riscv_extra
+    riscv_instr_decl
+    riscv_lower_addressing
+    riscv_lowering
+    riscv
+    riscv_params_common
+    riscv_params_core
+    riscv_params
+    riscv_stack_zeroization
+    sem_op_typed
+    sem_params
+    sem_params_of_arch_extra
+    sem_type
+    seq_extra
+    seq
+    sha256
+    shift_kind
+    slh_lowering
+    slh_ops
+    sopn
+    Specif
+    ssralg
+    ssrbool
+    ssreflect
+    ssrfun
+    ssrint
+    ssrnat
+    ssrnum
+    stack_alloc
+    stack_alloc_params
+    stack_zeroization
+    stack_zero_strategy
+    std
+    String0
+    Sumbool
+    syscall
+    syscall_sem
+    tagged
+    tunneling
+    tuple
+    type
+    Uint0
+    unionfind
+    unrolling
+    utils0
+    values
+    var0
+    varmap
+    waes
+    warray_
+    wint_int
+    wint_word
+    word0
+    word
+    word_ssrZ
+    wsize
+    x86_decl
+    x86_extra
+    x86_instr_decl
+    x86_lowering
+    x86
+    x86_params
+    x86_stack_zeroization
+    xseq
+    Zpower))
diff --git a/proofs/lang/extraction.v b/proofs/extraction/extraction.v
similarity index 95%
rename from proofs/lang/extraction.v
rename to proofs/extraction/extraction.v
index 4ccb97553e..9fba945054 100644
--- a/proofs/lang/extraction.v
+++ b/proofs/extraction/extraction.v
@@ -1,4 +1,4 @@
-Require jasmin_compiler.
+From jasmin_compiler Require jasmin_compiler.
 (* Do not “Require” other modules from Jasmin here:
    expand the jasmin_compiler module instead. *)
 
@@ -14,8 +14,8 @@ Extraction Inline ssrbool.is_left.
 Extraction Inline ssrbool.predT ssrbool.pred_of_argType.
 Extraction Inline ssrbool.idP.
 
-Extraction Inline utils.assert.
-Extraction Inline utils.Result.bind.
+Extraction Inline result.assert.
+Extraction Inline result.Result.bind.
 Extraction Inline Datatypes.implb.
 
 Extract Constant strings.ascii_eqb => "Char.equal".
@@ -53,8 +53,6 @@ Extract Constant ident.Cident.id_kind => "CoreIdent.Cident.id_kind".
 
 Extract Constant ident.Cident.spill_to_mmx => "CoreIdent.Cident.spill_to_mmx".
 
-Set Extraction Output Directory "lang/ocaml".
-
 Extraction Blacklist String List Nat Uint63 Utils Var Array.
 
 Separate Extraction
diff --git a/proofs/itrees/_CoqProject b/proofs/itrees/_CoqProject
new file mode 100644
index 0000000000..7a5f39e1c8
--- /dev/null
+++ b/proofs/itrees/_CoqProject
@@ -0,0 +1,20 @@
+-R ../_build/default/common common
+
+-R ../_build/default/itrees itrees
+
+-arg "-set" -arg "'Uniform Inductive Parameters'"
+-arg "-set" -arg "'Implicit Arguments'"
+-arg "-unset" -arg "'Strict Implicit'"
+-arg "-unset" -arg "'Printing Implicit Defensive'"
+-arg "-w -notation-overridden"
+-arg "-w -extraction-reserved-identifier"
+-arg "-w -extraction-opaque-accessed"
+-arg "-w -ambiguous-paths"
+-arg "-w -redundant-canonical-projection"
+-arg "-w -projection-no-head-constant"
+-arg "-w -postfix-notation-not-level-1"
+-arg "-w -deprecated-since-mathcomp-2.3.0"
+-arg "-w -deprecated-since-mathcomp-2.4.0"
+-arg "-w -deprecated-from-Coq"
+-arg "-w -deprecated-dirpath-Coq"
+
diff --git a/proofs/itrees/dune b/proofs/itrees/dune
new file mode 100644
index 0000000000..e4ed659426
--- /dev/null
+++ b/proofs/itrees/dune
@@ -0,0 +1,3 @@
+(coq.theory
+  (name itrees)
+  (theories elpi_elpi ExtLib ITree Paco common))
diff --git a/proofs/itrees/it_exec.v b/proofs/itrees/it_exec.v
index e5f4260341..1e5f1da86f 100644
--- a/proofs/itrees/it_exec.v
+++ b/proofs/itrees/it_exec.v
@@ -20,7 +20,7 @@ From ITree Require Import
      Eq.Eqit
      Eq.Paco2.
 
-Require Import utils.
+From common Require Import result.
 
 Import ITreeNotations.
 Local Open Scope itree_scope.
diff --git a/proofs/jasmin_compiler/_CoqProject b/proofs/jasmin_compiler/_CoqProject
new file mode 100644
index 0000000000..b45833b940
--- /dev/null
+++ b/proofs/jasmin_compiler/_CoqProject
@@ -0,0 +1,28 @@
+-R ../_build/default/arch arch
+-R ../_build/default/common common
+-R ../_build/default/compiler compiler
+-R ../_build/default/compiler/armv7 armv7
+-R ../_build/default/compiler/riscv riscv
+-R ../_build/default/compiler/x86 x86
+-R ../_build/default/lang lang
+-R ../_build/default/itrees itrees
+-R ../_build/default/ssrmisc ssrmisc
+-R ../_build/default/thirdparty thirdparty
+
+-R ../_build/default/jasmin_compiler jasmin_compiler
+
+-arg "-set" -arg "'Uniform Inductive Parameters'"
+-arg "-set" -arg "'Implicit Arguments'"
+-arg "-unset" -arg "'Strict Implicit'"
+-arg "-unset" -arg "'Printing Implicit Defensive'"
+-arg "-w -notation-overridden"
+-arg "-w -extraction-reserved-identifier"
+-arg "-w -extraction-opaque-accessed"
+-arg "-w -ambiguous-paths"
+-arg "-w -redundant-canonical-projection"
+-arg "-w -projection-no-head-constant"
+-arg "-w -postfix-notation-not-level-1"
+-arg "-w -deprecated-since-mathcomp-2.3.0"
+-arg "-w -deprecated-since-mathcomp-2.4.0"
+-arg "-w -deprecated-from-Coq"
+-arg "-w -deprecated-dirpath-Coq"
diff --git a/proofs/jasmin_compiler/dune b/proofs/jasmin_compiler/dune
new file mode 100644
index 0000000000..157e1fc6e5
--- /dev/null
+++ b/proofs/jasmin_compiler/dune
@@ -0,0 +1,3 @@
+(coq.theory
+  (name jasmin_compiler)
+  (theories compiler lang armv7 riscv x86))
diff --git a/proofs/jasmin_compiler/jasmin_compiler.v b/proofs/jasmin_compiler/jasmin_compiler.v
new file mode 100644
index 0000000000..caebd4e1c1
--- /dev/null
+++ b/proofs/jasmin_compiler/jasmin_compiler.v
@@ -0,0 +1,8 @@
+(** This module is meant as the minimal dependency of extracted code. *)
+From compiler Require compiler.
+From lang Require psem_defs.
+From armv7 Require arm_params.
+From x86 Require x86_params.
+From riscv Require riscv_params.
+From arch Require sem_params_of_arch_extra.
+From compiler Require wint_int.
diff --git a/proofs/lang/_CoqProject b/proofs/lang/_CoqProject
new file mode 100644
index 0000000000..9c9a462abd
--- /dev/null
+++ b/proofs/lang/_CoqProject
@@ -0,0 +1,22 @@
+-R ../_build/default/common common
+-R ../_build/default/itrees itrees
+-R ../_build/default/ssrmisc ssrmisc
+-R ../_build/default/thirdparty thirdparty
+
+-R ../_build/default/lang lang
+
+-arg "-set" -arg "'Uniform Inductive Parameters'"
+-arg "-set" -arg "'Implicit Arguments'"
+-arg "-unset" -arg "'Strict Implicit'"
+-arg "-unset" -arg "'Printing Implicit Defensive'"
+-arg "-w -notation-overridden"
+-arg "-w -extraction-reserved-identifier"
+-arg "-w -extraction-opaque-accessed"
+-arg "-w -ambiguous-paths"
+-arg "-w -redundant-canonical-projection"
+-arg "-w -projection-no-head-constant"
+-arg "-w -postfix-notation-not-level-1"
+-arg "-w -deprecated-since-mathcomp-2.3.0"
+-arg "-w -deprecated-since-mathcomp-2.4.0"
+-arg "-w -deprecated-from-Coq"
+-arg "-w -deprecated-dirpath-Coq"
diff --git a/proofs/lang/core_logics.v b/proofs/lang/core_logics.v
index 46d9deb5ea..4ec75dd664 100644
--- a/proofs/lang/core_logics.v
+++ b/proofs/lang/core_logics.v
@@ -17,7 +17,7 @@ From ITree Require Import
 
 From mathcomp Require Import ssreflect ssrfun ssrbool.
 
-Require Import xrutt xrutt_facts rutt_extras.
+From itrees Require Import xrutt xrutt_facts rutt_extras.
 
 Notation prepred E := (forall T, E T -> Prop).
 Notation postpred E := (forall T, E T -> T -> Prop).
diff --git a/proofs/lang/dune b/proofs/lang/dune
new file mode 100644
index 0000000000..22f3d3c7ae
--- /dev/null
+++ b/proofs/lang/dune
@@ -0,0 +1,3 @@
+(coq.theory
+  (name lang)
+  (theories HB mathcomp elpi elpi_elpi Paco itrees ssrmisc thirdparty))
diff --git a/proofs/lang/expr.v b/proofs/lang/expr.v
index 4ad274b0ff..27ab196a77 100644
--- a/proofs/lang/expr.v
+++ b/proofs/lang/expr.v
@@ -2,11 +2,11 @@
 From elpi.apps Require Import derive.std.
 From HB Require Import structures.
 From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat eqtype div ssralg.
-Require Import oseq.
+From ssrmisc Require Import oseq.
 From Coq Require Export ZArith Setoid Morphisms.
 From mathcomp Require Import word_ssrZ.
 Require Export strings word utils type ident var global sem_type slh_ops sopn syscall.
-Require Import xseq.
+From thirdparty Require Import xseq.
 Import Utf8 ZArith.
 
 Local Unset Elimination Schemes.
diff --git a/proofs/lang/fexpr_facts.v b/proofs/lang/fexpr_facts.v
index 32acf0a230..c6132358d2 100644
--- a/proofs/lang/fexpr_facts.v
+++ b/proofs/lang/fexpr_facts.v
@@ -1,5 +1,5 @@
 From Coq Require Import Utf8.
-Require Import oseq.
+From ssrmisc Require Import oseq.
 From mathcomp Require Import ssreflect ssrfun ssrbool.
 Require Import fexpr fexpr_sem.
 Require Import expr psem.
diff --git a/proofs/lang/global.v b/proofs/lang/global.v
index 1e3b9c7ac7..61b7396b24 100644
--- a/proofs/lang/global.v
+++ b/proofs/lang/global.v
@@ -2,7 +2,8 @@
 From mathcomp Require Import ssreflect ssrfun ssrbool ssralg.
 From mathcomp Require Import word_ssrZ.
 From Coq Require Import ZArith.
-Require Export xseq word utils var warray_.
+From thirdparty Require Export xseq.
+Require Export word utils var warray_.
 
 (* ---------------------------------------------------------------------- *)
 
diff --git a/proofs/lang/hoare_logic.v b/proofs/lang/hoare_logic.v
index 76e2da2d84..c376969b61 100644
--- a/proofs/lang/hoare_logic.v
+++ b/proofs/lang/hoare_logic.v
@@ -24,8 +24,8 @@ Import Monads.
 Import MonadNotation.
 Local Open Scope monad_scope.
 
-
-Require Import expr psem_defs oseq compiler_util.
+From ssrmisc Require Import oseq.
+Require Import expr psem_defs.
 (* needed for the last lemma *)
 Require Import psem_core.
 
diff --git a/proofs/lang/it_sems_core.v b/proofs/lang/it_sems_core.v
index 4c57a7cf4e..57364ea808 100644
--- a/proofs/lang/it_sems_core.v
+++ b/proofs/lang/it_sems_core.v
@@ -9,7 +9,8 @@ Import Basics.Monads.
 
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype.
 
-Require Import expr psem_defs psem_core it_exec.
+Require Import expr psem_defs psem_core.
+From itrees Require Import it_exec.
 
 Import MonadNotation.
 Local Open Scope monad_scope.
diff --git a/proofs/arch/label.v b/proofs/lang/label.v
similarity index 100%
rename from proofs/arch/label.v
rename to proofs/lang/label.v
diff --git a/proofs/lang/linear_sem.v b/proofs/lang/linear_sem.v
index 075fef0704..718decb0eb 100644
--- a/proofs/lang/linear_sem.v
+++ b/proofs/lang/linear_sem.v
@@ -5,8 +5,8 @@
 From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat ssralg.
 From Coq Require Import ZArith Utf8.
 Import Relations.
-Require oseq.
-Require Import psem fexpr_sem compiler_util label one_varmap linear sem_one_varmap.
+From ssrmisc Require oseq.
+Require Import psem fexpr_sem label one_varmap linear sem_one_varmap.
 
 Import Memory.
 
diff --git a/proofs/lang/memory_model.v b/proofs/lang/memory_model.v
index 77fd0b94fd..1fd25c3803 100644
--- a/proofs/lang/memory_model.v
+++ b/proofs/lang/memory_model.v
@@ -5,7 +5,7 @@ From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat seq div eqtype.
 From mathcomp Require Import ssralg word_ssrZ.
 Require Import strings word utils.
 Import Utf8 ZArith Lia.
-Require Import ssrring.
+From thirdparty Require Import ssrring.
 
 Local Open Scope Z_scope.
 
diff --git a/proofs/lang/one_varmap.v b/proofs/lang/one_varmap.v
index 456782705f..8893453dec 100644
--- a/proofs/lang/one_varmap.v
+++ b/proofs/lang/one_varmap.v
@@ -1,7 +1,7 @@
 (** This module defines common definitions related to the “one-varmap” intermediate language.
 This language is structured (as jasmin-source) and is used just before linearization: there is a single environment (varmap) shared across function calls.
 *)
-Require Import expr compiler_util.
+Require Import expr.
 Import Utf8.
 From mathcomp Require Import ssreflect ssrfun ssrbool.
 
diff --git a/proofs/lang/psem.v b/proofs/lang/psem.v
index 8abbebddc8..3976a1c372 100644
--- a/proofs/lang/psem.v
+++ b/proofs/lang/psem.v
@@ -2,7 +2,7 @@
 
 (* ** Imports and settings *)
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssralg.
-Require Import xseq.
+From thirdparty Require Import xseq.
 Require Export array type expr gen_map warray_ sem_type sem_op_typed values varmap expr_facts low_memory syscall_sem psem_defs.
 Require Export psem_core it_sems_core hoare_logic relational_logic.
 Require Export
diff --git a/proofs/lang/psem_core.v b/proofs/lang/psem_core.v
index 162d348595..3ccb903520 100644
--- a/proofs/lang/psem_core.v
+++ b/proofs/lang/psem_core.v
@@ -2,7 +2,7 @@
 
 (* ** Imports and settings *)
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssralg.
-Require Import xseq.
+From thirdparty Require Import xseq.
 Require Export array type expr gen_map warray_ sem_type sem_op_typed values varmap expr_facts low_memory syscall_sem psem_defs.
 Require Export
   flag_combination
diff --git a/proofs/lang/psem_defs.v b/proofs/lang/psem_defs.v
index c3f15e267e..e27b8e569f 100644
--- a/proofs/lang/psem_defs.v
+++ b/proofs/lang/psem_defs.v
@@ -2,7 +2,7 @@
 
 (* ** Imports and settings *)
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssralg.
-Require Import xseq.
+From thirdparty Require Import xseq.
 Require Export array type expr gen_map low_memory warray_ sem_type sem_op_typed values varmap low_memory syscall_sem.
 Require Export
   flag_combination
diff --git a/proofs/lang/relational_logic.v b/proofs/lang/relational_logic.v
index 15e0b42778..94d56a117b 100644
--- a/proofs/lang/relational_logic.v
+++ b/proofs/lang/relational_logic.v
@@ -19,8 +19,9 @@ Import Monads.
 Import MonadNotation.
 Local Open Scope monad_scope.
 
-Require Import xrutt xrutt_facts.
-Require Import expr psem_defs psem_core oseq compiler_util.
+From itrees Require Import xrutt xrutt_facts.
+From ssrmisc Require Import oseq.
+Require Import expr psem_defs psem_core.
 Require Import it_sems_core core_logics hoare_logic.
 Import Utf8.
 
diff --git a/proofs/lang/sem_type.v b/proofs/lang/sem_type.v
index 5876a81524..06ca76e863 100644
--- a/proofs/lang/sem_type.v
+++ b/proofs/lang/sem_type.v
@@ -3,7 +3,7 @@
 (* ** Imports and settings *)
 From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat eqtype ssralg.
 From mathcomp Require Import word_ssrZ.
-Require Import xseq.
+From thirdparty Require Import xseq.
 Require Export strings warray_.
 Import Utf8.
 
diff --git a/proofs/lang/utils.v b/proofs/lang/utils.v
index eacec1607e..45c0b271e4 100644
--- a/proofs/lang/utils.v
+++ b/proofs/lang/utils.v
@@ -5,7 +5,9 @@ From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat eqtype choice.
 From mathcomp Require Import fintype finfun.
 From Coq.Unicode Require Import Utf8.
 From Coq Require Import ZArith Zwf Setoid Morphisms CMorphisms CRelationClasses.
-Require Import xseq oseq.
+From thirdparty Require Import xseq.
+From ssrmisc Require Import oseq.
+From common Require Export result.
 From mathcomp Require Import word_ssrZ.
 
 
@@ -119,104 +121,6 @@ Instance and3_iff_morphism :
   Proper (iff ==> iff ==> iff ==> iff) and3.
 Proof. by move=> ?? h1 ?? h2 ?? h3; split => -[] /h1 ? /h2 ? /h3. Qed.
 
-(* ** Result monad
- * -------------------------------------------------------------------- *)
-
-Variant result (E : Type) (A : Type) : Type :=
-| Ok of A
-| Error of E.
-
-Arguments Error {E} {A} s.
-
-Definition is_ok (E A:Type) (r:result E A) := if r is Ok a then true else false.
-
-Lemma is_ok_ok (E A:Type) (a:A) : is_ok (Ok E a).
-Proof. done. Qed.
-#[global]
-Hint Resolve is_ok_ok : core.
-
-Lemma is_okP (E A:Type) (r:result E A) : reflect (exists (a:A), r = Ok E a) (is_ok r).
-Proof.
-  case: r => /=; constructor; first by eauto.
-  by move=> [].
-Qed.
-
-Module Result.
-
-Definition apply eT aT rT (f : aT -> rT) (x : rT) (u : result eT aT) :=
-  if u is Ok y then f y else x.
-
-Definition bind eT aT rT (f : aT -> result eT rT) g :=
-  match g with
-  | Ok x    => f x
-  | Error s => Error s
-  end.
-
-Definition map eT aT rT (f : aT -> rT) := bind (fun x => Ok eT (f x)).
-Definition default eT aT := @apply eT aT aT (fun x => x).
-
-Definition map_err
-  eT1 eT2 aT (f : eT1 -> eT2) (r : result eT1 aT) : result eT2 aT :=
-  match r with
-  | Ok x => Ok _ x
-  | Error e => Error (f e)
-  end.
-
-End Result.
-
-Definition o2r eT aT (e : eT) (o : option aT) :=
-  match o with
-  | None   => Error e
-  | Some x => Ok eT x
-  end.
-
-Notation rapp  := Result.apply.
-Notation rdflt := Result.default.
-Notation rbind := Result.bind.
-Notation rmap  := Result.map.
-Notation ok    := (@Ok _).
-
-Declare Scope result_scope.
-Delimit Scope result_scope with result.
-Open Scope result_scope.
-
-Notation "m >>= f" := (rbind f m) (at level 58, left associativity) : result_scope.
-Notation "'Let' x ':=' m 'in' body" := (m >>= (fun x => body)) (x name, at level 25) : result_scope.
-Notation "'Let:' x ':=' m 'in' body" := (m >>= (fun x => body)) (x strict pattern, at level 25) : result_scope.
-Notation "m >> n" := (rbind (λ _, n) m) (at level 30, right associativity, n at next level) : result_scope.
-
-Lemma bindA eT aT bT cT (f : aT -> result eT bT) (g: bT -> result eT cT) m:
-  m >>= f >>= g = m >>= (fun a => f a >>= g).
-Proof. case:m => //=. Qed.
-
-Lemma bind_eq eT aT rT (f1 f2 : aT -> result eT rT) m1 m2 :
-   m1 = m2 -> f1 =1 f2 -> m1 >>= f1 = m2 >>= f2.
-Proof. move=> <- Hf; case m1 => //=. Qed.
-
-Definition ok_inj {E A} {a a': A} (H: Ok E a = ok a') : a = a' :=
-  let 'Logic.eq_refl := H in Logic.eq_refl.
-
-Definition Error_inj {E A} (a a': E) (H: @Error E A a = Error a') : a = a' :=
-  let 'Logic.eq_refl := H in Logic.eq_refl.
-
-Definition assert E (b: bool) (e: E) : result E unit :=
-  if b then ok tt else Error e.
-
-Lemma assertP E b e u :
-  @assert E b e = ok u → b.
-Proof. by case: b. Qed.
-
-Arguments assertP {E b e u} _.
-
-Lemma map_errP eT1 eT2 aT (f : eT1 -> eT2) (r : result eT1 aT) x :
-  Result.map_err f r = ok x ->
-  r = ok x.
-Proof. by case: r => //= ? [->]. Qed.
-Arguments map_errP {_ _ _ _ _ _}.
-
-Variant error :=
- | ErrOob | ErrAddrUndef | ErrAddrInvalid | ErrStack | ErrType | ErrArith | ErrSemUndef.
-
 Definition exec t := result error t.
 
 Definition type_error {t} := @Error _ t ErrType.
diff --git a/proofs/lang/values.v b/proofs/lang/values.v
index f404087f26..ded9f334a8 100644
--- a/proofs/lang/values.v
+++ b/proofs/lang/values.v
@@ -3,7 +3,7 @@
 (* ** Imports and settings *)
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssralg.
 From mathcomp Require Import word_ssrZ.
-Require Import xseq.
+From thirdparty Require Import xseq.
 Require Export warray_ word sem_type.
 Import Utf8.
 
diff --git a/proofs/lang/warray_.v b/proofs/lang/warray_.v
index b447346f4e..cd394eb1a5 100644
--- a/proofs/lang/warray_.v
+++ b/proofs/lang/warray_.v
@@ -6,7 +6,7 @@ From HB Require Import structures.
 From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat eqtype div ssralg.
 From mathcomp Require Import word_ssrZ.
 From Coq Require Export ZArith Setoid Morphisms.
-Require Import xseq.
+From thirdparty Require Import xseq.
 Require Export utils array gen_map type word memory_model.
 Import Utf8 ZArith Lia.
 
diff --git a/proofs/ssrmisc/_CoqProject b/proofs/ssrmisc/_CoqProject
new file mode 100644
index 0000000000..dc53747526
--- /dev/null
+++ b/proofs/ssrmisc/_CoqProject
@@ -0,0 +1,17 @@
+-R ../_build/default/ssrmisc ssrmisc
+
+-arg "-set" -arg "'Uniform Inductive Parameters'"
+-arg "-set" -arg "'Implicit Arguments'"
+-arg "-unset" -arg "'Strict Implicit'"
+-arg "-unset" -arg "'Printing Implicit Defensive'"
+-arg "-w -notation-overridden"
+-arg "-w -extraction-reserved-identifier"
+-arg "-w -extraction-opaque-accessed"
+-arg "-w -ambiguous-paths"
+-arg "-w -redundant-canonical-projection"
+-arg "-w -projection-no-head-constant"
+-arg "-w -postfix-notation-not-level-1"
+-arg "-w -deprecated-since-mathcomp-2.3.0"
+-arg "-w -deprecated-since-mathcomp-2.4.0"
+-arg "-w -deprecated-from-Coq"
+-arg "-w -deprecated-dirpath-Coq"
diff --git a/proofs/ssrmisc/dune b/proofs/ssrmisc/dune
new file mode 100644
index 0000000000..58b48f77ed
--- /dev/null
+++ b/proofs/ssrmisc/dune
@@ -0,0 +1,3 @@
+(coq.theory
+  (name ssrmisc)
+  (theories elpi elpi_elpi HB mathcomp))
diff --git a/proofs/ssrmisc/seq_extra.v b/proofs/ssrmisc/seq_extra.v
index a43bebd88f..7a8270ff79 100644
--- a/proofs/ssrmisc/seq_extra.v
+++ b/proofs/ssrmisc/seq_extra.v
@@ -1,6 +1,7 @@
-From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat seq.
 From Coq Require Import Utf8.
-Require Import oseq utils.
+From Coq Require Import List.
+From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat seq.
+Require Import oseq.
 
 
 Section PairFoldLeft.
@@ -69,6 +70,12 @@ Proof. by elim: s n => [|x s IHs] //= [|n] /=; rewrite ?drop0. Qed.
 
 Section AllProps.
 
+(* FIXME: duplicated from lang/utils.v to remove dependency *)
+Lemma List_Forall_inv A (P: A → Prop) m :
+  List.Forall P m →
+  match m with [::] => True | x :: m' => P x ∧ List.Forall P m' end.
+Proof. by case. Qed.
+
   Lemma allE (T: Type) (p: pred T) m :
     reflect (List.Forall p m) (all p m).
   Proof.
diff --git a/proofs/thirdparty/_CoqProject b/proofs/thirdparty/_CoqProject
new file mode 100644
index 0000000000..4bdb9f288f
--- /dev/null
+++ b/proofs/thirdparty/_CoqProject
@@ -0,0 +1,17 @@
+-R ../_build/default/thirdparty thirdparty
+
+-arg "-set" -arg "'Uniform Inductive Parameters'"
+-arg "-set" -arg "'Implicit Arguments'"
+-arg "-unset" -arg "'Strict Implicit'"
+-arg "-unset" -arg "'Printing Implicit Defensive'"
+-arg "-w -notation-overridden"
+-arg "-w -extraction-reserved-identifier"
+-arg "-w -extraction-opaque-accessed"
+-arg "-w -ambiguous-paths"
+-arg "-w -redundant-canonical-projection"
+-arg "-w -projection-no-head-constant"
+-arg "-w -postfix-notation-not-level-1"
+-arg "-w -deprecated-since-mathcomp-2.3.0"
+-arg "-w -deprecated-since-mathcomp-2.4.0"
+-arg "-w -deprecated-from-Coq"
+-arg "-w -deprecated-dirpath-Coq"
diff --git a/proofs/thirdparty/dune b/proofs/thirdparty/dune
new file mode 100644
index 0000000000..0b09d84fdf
--- /dev/null
+++ b/proofs/thirdparty/dune
@@ -0,0 +1,3 @@
+(coq.theory
+  (name thirdparty)
+  (theories elpi elpi_elpi HB mathcomp))
diff --git a/proofs/3rdparty/ssrring.v b/proofs/thirdparty/ssrring.v
similarity index 100%
rename from proofs/3rdparty/ssrring.v
rename to proofs/thirdparty/ssrring.v
diff --git a/proofs/3rdparty/xseq.v b/proofs/thirdparty/xseq.v
similarity index 100%
rename from proofs/3rdparty/xseq.v
rename to proofs/thirdparty/xseq.v