diff --git a/tests/spec/extend_extern.i b/tests/spec/extend_extern.i
new file mode 100644
index 0000000000000000000000000000000000000000..8dffe2261770f824cb6dd7c1ffbf81597c9f15a1
--- /dev/null
+++ b/tests/spec/extend_extern.i
@@ -0,0 +1,7 @@
+/* run.config
+   MACRO: PTEST_MAKE_MODULE make FRAMAC_USER_OFLAGS="-package why3" FRAMAC_USER_BFLAGS="-package why3"
+   MODULE: @PTEST_DIR@/@PTEST_NAME@.cmxs
+   OPT:
+ */
+/*@ predicate load(char * x) = \true ; */
+/*@ why3 load("List"); */
diff --git a/tests/spec/extend_extern.ml b/tests/spec/extend_extern.ml
new file mode 100644
index 0000000000000000000000000000000000000000..70f1ad660c25adcf657ff3b007b5cd5ec6ecf8fb
--- /dev/null
+++ b/tests/spec/extend_extern.ml
@@ -0,0 +1,22 @@
+open Logic_typing
+open Cil_types
+
+let load_theory = function
+  | { pred_content = Papp (_, [], [ { term_node = TConst(LStr _name) } ] ) } ->
+    let open Why3 in ignore (
+      Theory.import_namespace Theory.empty_ns [_name]
+    )
+  | _ -> assert false
+
+let typing ~typing_context ~loc lexprs =
+  ignore loc ;
+  let type_predicate =
+    typing_context.type_predicate typing_context (Lenv.empty ())
+  in
+  let predicates = List.map type_predicate lexprs in
+  List.iter load_theory predicates ;
+  Ext_preds predicates
+
+
+let () =
+  Logic_typing.register_global_extension "why3" false typing