diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 12d26b50efbbee94f783e89d75faa44dab37178f..7b1a6642db0d34ac5f7bc9af6867203f3dcbcd6e 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -22,6 +22,7 @@ lrust-coq8.6:
   - master
   - ci
   - /^ralf/ci//
+  - jh/undiscriminated_hintdb
   artifacts:
     paths:
     - build-time.txt
diff --git a/theories/typing/lft_contexts.v b/theories/typing/lft_contexts.v
index ae8dbde0ee8fd9cacffa0302dde4633f3aa03d81..0cd42e35de775dd360a44a12485826dc9ff79a1b 100644
--- a/theories/typing/lft_contexts.v
+++ b/theories/typing/lft_contexts.v
@@ -454,6 +454,9 @@ End elctx_incl.
 
 Arguments elctx_incl {_ _ _} _%EL _%LL _%EL _%EL.
 
+Create HintDb lrust_typing.
+Create HintDb lrust_typing_merge.
+
 (* We first try to solve everything without the merging rules, and
    then start from scratch with them.
 
@@ -463,8 +466,6 @@ Arguments elctx_incl {_ _ _} _%EL _%LL _%EL _%EL.
 Ltac solve_typing :=
   (typeclasses eauto with lrust_typing typeclass_instances core; fail) ||
   (typeclasses eauto with lrust_typing lrust_typing_merge typeclass_instances core; fail).
-Create HintDb lrust_typing discriminated.
-Create HintDb lrust_typing_merge discriminated.
 
 Hint Constructors Forall Forall2 elem_of_list : lrust_typing.
 Hint Resolve of_val_unlock : lrust_typing.