diff --git a/.gitlab/ci/coq.yml b/.gitlab/ci/coq.yml
index 0516126deb2ae175d171fb15c7b2ea52f370211b..8607c9fb20f5ace7db425b26b5541bb46577a7e5 100644
--- a/.gitlab/ci/coq.yml
+++ b/.gitlab/ci/coq.yml
@@ -1,8 +1,26 @@
+# Verify that the protocol's environment, as imported by `coq-of-ocaml`,
+# compiles in Coq
+coq:environment:
+  extends: .test_template
+  needs: []
+  script:
+    # We only need merlin to be able to read the cmt files, the @check target
+    # provides this
+    - dune build @src/proto_alpha/lib_protocol/check
+    - cd _build/default/src/lib_protocol_environment/sigs
+    - tail -n +2 v3.ml | head -n -2 | grep -v "\# 1" > environment.mli
+    - coq-of-ocaml -config ../../../../../src/proto_alpha/lib_protocol/coq-of-ocaml/config-environment.json environment.mli || true
+    - cat Environment.v
+    - coqc Environment.v
+  retry: 0
+
+# Verify that the files of the protocol do not produce warnings
+# with `coq-of-ocaml`
 coq:lint:
   extends: .test_template
   needs: []
   script:
-    # we only need merlin to be able to read the cmt files, the @check target
+    # We only need merlin to be able to read the cmt files, the @check target
     # provides this
     - dune build @src/proto_alpha/lib_protocol/check
     - cd src/proto_alpha/lib_protocol
diff --git a/src/proto_alpha/lib_protocol/coq-of-ocaml/config-environment.json b/src/proto_alpha/lib_protocol/coq-of-ocaml/config-environment.json
new file mode 100644
index 0000000000000000000000000000000000000000..00ce3cfbd78dac03e16e9cbd925782a227e5fee3
--- /dev/null
+++ b/src/proto_alpha/lib_protocol/coq-of-ocaml/config-environment.json
@@ -0,0 +1,72 @@
+{
+  "alias_barrier_modules": [
+    "Tezos_protocol_environment_alpha__Environment"
+  ],
+  "constructor_map": [
+    ["public_key_hash", "Ed25519", "Ed25519Hash"],
+    ["public_key_hash", "P256", "P256Hash"],
+    ["public_key_hash", "Secp256k1", "Secp256k1Hash"]
+  ],
+  "error_category_blacklist": [
+    "extensible_type",
+    "side_effect"
+  ],
+  "error_message_blacklist": [
+    "Polymorphic variant types are defined as standard algebraic types",
+    "Sub-modules in included signatures are not handled well yet.",
+    "No type known for the following variants:"
+  ],
+  "escape_value": [
+    "a",
+    "alloc",
+    "b",
+    "baking_rights_query",
+    "case",
+    "cons",
+    "descr",
+    "diff",
+    "elt",
+    "endorsing_rights_query",
+    "eq",
+    "error",
+    "field",
+    "fixed",
+    "fp",
+    "frozen_balance",
+    "handler",
+    "has_lazy_storage",
+    "hash",
+    "info",
+    "init",
+    "integral",
+    "internal_gas",
+    "json",
+    "json_schema",
+    "judgement",
+    "key",
+    "lazy_expr",
+    "level_query",
+    "list_query",
+    "namespace",
+    "nonce",
+    "query",
+    "p",
+    "parametric",
+    "r",
+    "raw",
+    "seed",
+    "sequence",
+    "snapshot",
+    "stack",
+    "storage",
+    "storage_error",
+    "t",
+    "tc_context",
+    "trace",
+    "type_logger"
+  ],
+  "variant_types": [
+    ["Dir", "Context.key_or_dir"],
+    ["Key", "Context.key_or_dir"]
+  ]
+}