diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 254f7fadc17f92855af435144c37303826d431a7..165b33a5a2a9ca4490b0171eec95d4fc7c4ef1c4 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -11,6 +11,7 @@ tests:
   script:
   - if [ ! -d _opam ]; then echo "no local switch in the CI cache, we setup a new switch"; opam switch create --yes --no-install . ocaml-base-compiler.4.13.1; fi
   - eval $(opam env)
+  - opam switch
   - sudo apt-get update
   - sudo apt install -y protobuf-compiler
   - opam repository add remote https://opam.ocaml.org
diff --git a/src/language.ml b/src/language.ml
index bd67d917830d164cf679c11c66130f86a30808f7..20d78f6af3d437388b6e461fb6b9bd3dce8fb3e3 100644
--- a/src/language.ml
+++ b/src/language.ml
@@ -9,7 +9,7 @@ open Base
 
 (* -- Support for the NNet and ONNX neural network formats. *)
 
-type ioshape = {
+type nnshape = {
   nb_inputs : int;
   nb_outputs : int;
   ty_data : Ty.ty;
@@ -19,12 +19,12 @@ type ioshape = {
 let loaded_nets = Term.Hls.create 10
 let lookup_loaded_nets = Term.Hls.find_opt loaded_nets
 
-let register_astuple nb_inputs nb_outputs filename env =
-  let net = Pmodule.read_module env [ "caisar" ] "IOShape" in
+let register_nn_as_tuple nb_inputs nb_outputs filename env =
+  let net = Pmodule.read_module env [ "caisar" ] "NN" in
   let ioshape_input_type =
     Ty.ty_app Theory.(ns_find_ts net.mod_theory.th_export [ "input_type" ]) []
   in
-  let id_as_tuple = Ident.id_fresh "AsTuple" in
+  let id_as_tuple = Ident.id_fresh "NNasTuple" in
   let th_uc = Pmodule.create_module env id_as_tuple in
   let th_uc = Pmodule.use_export th_uc net in
   let ls_net_apply =
@@ -40,19 +40,19 @@ let register_astuple nb_inputs nb_outputs filename env =
     Pmodule.add_pdecl ~vc:false th_uc
       (Pdecl.create_pure_decl (Decl.create_param_decl ls_net_apply))
   in
-  Wstdlib.Mstr.singleton "AsTuple" (Pmodule.close_module th_uc)
+  Wstdlib.Mstr.singleton "NNasTuple" (Pmodule.close_module th_uc)
 
 let nnet_parser env _ filename _ =
   let model = Nnet.parse filename in
   match model with
   | Error s -> Loc.errorm "%s" s
-  | Ok model -> register_astuple model.n_inputs model.n_outputs filename env
+  | Ok model -> register_nn_as_tuple model.n_inputs model.n_outputs filename env
 
 let onnx_parser env _ filename _ =
   let model = Onnx.parse filename in
   match model with
   | Error s -> Loc.errorm "%s" s
-  | Ok model -> register_astuple model.n_inputs model.n_outputs filename env
+  | Ok model -> register_nn_as_tuple model.n_inputs model.n_outputs filename env
 
 let register_nnet_support () =
   Env.register_format ~desc:"NNet format (ReLU only)" Pmodule.mlw_language
diff --git a/src/language.mli b/src/language.mli
index 070aef66e11545814eb2a4924b8e2c648d60054e..157c53a964fe57a0b84d1230baf36f9e7fd98f3e 100644
--- a/src/language.mli
+++ b/src/language.mli
@@ -6,14 +6,14 @@
 
 open Why3
 
-type ioshape = {
+type nnshape = {
   nb_inputs : int;
   nb_outputs : int;
   ty_data : Ty.ty;
   filename : string;
 }
 
-val lookup_loaded_nets : Term.lsymbol -> ioshape option
+val lookup_loaded_nets : Term.lsymbol -> nnshape option
 (** @return the filename of a nnet Why3 representation. *)
 
 val register_nnet_support : unit -> unit
diff --git a/stdlib/caisar.mlw b/stdlib/caisar.mlw
index 9166a2a923317ff4bd192e7a27bba880dd625628..5de155d87e928dbc7e5589bdb62fcb830450f016 100644
--- a/stdlib/caisar.mlw
+++ b/stdlib/caisar.mlw
@@ -1,4 +1,4 @@
-theory IOShape
+theory NN
   use ieee_float.Float64
   type input_type = t
 end
diff --git a/tests/marabou.t b/tests/marabou.t
index ffc8f76fa172b42c341cb485ddfbbc84117d2dbd..2d7b6bf3f0c60c5b76e36b33c75dae626b543a38 100644
--- a/tests/marabou.t
+++ b/tests/marabou.t
@@ -19,9 +19,9 @@ Test verify
 
   $ caisar verify -L . --format whyml --prover=Marabou - 2>&1 <<EOF | sed 's/\/tmp\/[a-z0-9_./]*/$TMPFILE/'
   > theory T
-  >   use TestNetwork.AsTuple
+  >   use TestNetwork.NNasTuple
   >   use ieee_float.Float64
-  >   use caisar.IOShape
+  >   use caisar.NN
   > 
   >   goal G: forall x1 x2 x3 x4 x5.
   >      (0.0:t) .< x1 .< (0.5:t) ->
diff --git a/tests/simple.t b/tests/simple.t
index ed3d8805237a465f83a0201fb3e3ac2c55b76002..a49bc1f25761ec39850eca84bacbe4c8ff22f9f4 100644
--- a/tests/simple.t
+++ b/tests/simple.t
@@ -19,9 +19,9 @@ Test verify
 
   $ caisar verify -L . --format whyml --prover=PyRAT - 2>&1 <<EOF | sed 's/\/tmp\/[a-z0-9_./]*/$TMPFILE/'
   > theory T
-  >   use TestNetwork.AsTuple
+  >   use TestNetwork.NNasTuple
   >   use ieee_float.Float64
-  >   use caisar.IOShape
+  >   use caisar.NN
   > 
   >   goal G: forall x1 x2 x3 x4 x5.
   >      (0.0:t) .< x1 .< (0.5:t) ->
diff --git a/tests/simple_onnx.t b/tests/simple_onnx.t
index 5c6442dcde26cb32ec666d1c052e275b0831013d..7509548805f3310b454be91df2a0387d3d506476 100644
--- a/tests/simple_onnx.t
+++ b/tests/simple_onnx.t
@@ -19,9 +19,9 @@ Test verify
 
   $ caisar verify -L . --format whyml --prover=PyRAT - 2>&1 <<EOF | sed 's/\/tmp\/[a-z0-9_./]*/$TMPFILE/'
   > theory T
-  >   use TestNetworkONNX.AsTuple
+  >   use TestNetworkONNX.NNasTuple
   >   use ieee_float.Float64
-  >   use caisar.IOShape
+  >   use caisar.NN
   > 
   >   goal G: forall x1 x2 x3.
   >      (0.0:t) .< x1 .< (0.5:t) ->