diff --git a/apps/tc/elpi/create_tc_predicate.elpi b/apps/tc/elpi/create_tc_predicate.elpi
index ec12a888b..8b0004b81 100644
--- a/apps/tc/elpi/create_tc_predicate.elpi
+++ b/apps/tc/elpi/create_tc_predicate.elpi
@@ -55,7 +55,9 @@ attr->modes CoqModes :-
 attr->modes [].
 
 pred get-key-from-option i:prop, o:string. 
-get-key-from-option (get-option A _) A :- !.
+get-key-from-option (get-option A tt) A :- !.
+get-key-from-option (get-option "i" ff) "o" :- !.
+get-key-from-option (get-option "o" ff) "i" :- !.
 get-key-from-option A _ :- coq.error A "should be an option".
 
 pred declare-class-in-coq i:gref.
diff --git a/apps/tc/tests/classes_declare.v b/apps/tc/tests/classes_declare.v
index 56d10a5e2..db1f9f1b3 100644
--- a/apps/tc/tests/classes_declare.v
+++ b/apps/tc/tests/classes_declare.v
@@ -59,4 +59,17 @@ Section S3.
 
 End S3.
 
+Section S31.
+  #[mode(o=ff)] TC.Declare Class class31 (n : nat).
+  Instance inst31 : class31 0. Proof. apply Build_class31. Qed.
+
+  Goal exists x, class31 x. 
+  Proof.
+    eexists.
+    Succeed apply inst31.
+    Fail apply _.
+  Abort.
+
+End S31.
+