diff --git a/Changelog.md b/Changelog.md
index e1c8c652f..f77579134 100644
--- a/Changelog.md
+++ b/Changelog.md
@@ -12,6 +12,7 @@
 - Change `tc-instance`, now the type is `gref -> tc-priority -> tc-instance` i.e. the priority is not an integer anymore
 - New `coq.ltac.fresh-id` to generate fresh names in the proof context
 - New `@no-tc!` attribute supported by `coq.ltac.call-ltac1`
+- New `coq.TC.get-inst-prio` returns the `tc-priority` of an instance
 
 ### Apps 
 - New `tc` app providing an implementation of a type class solver written in elpi.
diff --git a/apps/tc/_CoqProject.test b/apps/tc/_CoqProject.test
index 6d683f46f..293e86d66 100644
--- a/apps/tc/_CoqProject.test
+++ b/apps/tc/_CoqProject.test
@@ -1,4 +1,5 @@
 -arg -w -arg -Not-added
+-arg -w -arg -TC.hints
 
 # Hack to see Coq-Elpi even if it is not installed yet
 -Q ../../theories elpi
diff --git a/apps/tc/elpi/alias.elpi b/apps/tc/elpi/alias.elpi
index 7f8844038..bf7f420ab 100644
--- a/apps/tc/elpi/alias.elpi
+++ b/apps/tc/elpi/alias.elpi
@@ -1,6 +1,8 @@
 /* license: GNU Lesser General Public License Version 2.1 or later           */
 /* ------------------------------------------------------------------------- */
 
+accumulate base.
+
 pred alias i:term, o:term.
 
 pred replace-with-alias.aux i:list term, o:list term, o:bool.
diff --git a/apps/tc/elpi/compiler.elpi b/apps/tc/elpi/compiler.elpi
index 504160b98..36faf5933 100644
--- a/apps/tc/elpi/compiler.elpi
+++ b/apps/tc/elpi/compiler.elpi
@@ -1,6 +1,9 @@
 /* license: GNU Lesser General Public License Version 2.1 or later           */
 /* ------------------------------------------------------------------------- */
 
+accumulate base.
+accumulate tc_aux.
+
 % returns the classes on which the current gref depends
 pred get-class-dependencies i:gref, o:list gref.
 get-class-dependencies GR Res :-
@@ -97,7 +100,7 @@ compile-aux (prod N T F) I RevPremises ListVar [] IsPositive IsHead Clause ff :-
         (L = [NewPremise | RevPremises])) (L = RevPremises),
     compile-aux (F p) I L [p | ListVar] [] IsPositive IsHead (C p) _.
 compile-aux Ty I RevPremises ListVar [] _ IsHead Clause tt :- 
-  not (is-option-active {oTC-use-pattern-fragment-compiler}), !,
+  not (is-option-active oTC-use-pattern-fragment-compiler), !,
   std.rev RevPremises Premises,
   coq.mk-app I {std.rev ListVar} AppInst,
   make-tc IsHead Ty AppInst Premises Clause.
diff --git a/apps/tc/elpi/create_tc_predicate.elpi b/apps/tc/elpi/create_tc_predicate.elpi
index 77ef64d7f..8e06a3d77 100644
--- a/apps/tc/elpi/create_tc_predicate.elpi
+++ b/apps/tc/elpi/create_tc_predicate.elpi
@@ -1,5 +1,9 @@
 /* license: GNU Lesser General Public License Version 2.1 or later           */
 /* ------------------------------------------------------------------------- */
+
+accumulate base.
+accumulate tc_aux.
+
 pred string->coq-mode i:string, o:hint-mode.
 string->coq-mode "bang" mode-ground :- !.
 string->coq-mode "plus" mode-input :- !.
@@ -14,14 +18,19 @@ coq-mode->elpi mode-ground (pr in "term"). % approximation
 coq-mode->elpi mode-input (pr in "term").
 coq-mode->elpi mode-output (pr out "term").
 
+% Here we build the elpi modes a class CL. If CL has either zero or more than
+% one mode, then we consider all its parameter to be in output mode. If the
+% class has exactly one mode, then it is considered for the signature of the
+% predicate for CL 
 pred modes-of-class i:gref, o:list (pair argument_mode string).
-modes-of-class ClassGr Modes :- 
-  coq.hints.modes ClassGr "typeclass_instances" CoqModesList,
+modes-of-class ClassGR Modes :- 
+  coq.hints.modes ClassGR "typeclass_instances" CoqModesList,
   not (CoqModesList = []),
-  std.assert! (CoqModesList = [HintModesFst]) "At the moment we only allow TC with one Hint Mode",
+  not (CoqModesList = [_,_|_], coq.warning "TC.Modes" "At the moment we only allow TC with at most 1 hint Mode (caused by class" {coq.gref->string ClassGR} ")"),
+  CoqModesList = [HintModesFst],
   std.append {std.map HintModesFst coq-mode->elpi} [pr out "term"] Modes.
-modes-of-class ClassGr Modes :- 
-  coq.env.typeof ClassGr ClassTy,
+modes-of-class ClassGR Modes :- 
+  coq.env.typeof ClassGR ClassTy,
   N is {coq.count-prods ClassTy} + 1, % + 1 for the solution
   list-init N (x\r\ r = (pr out "term")) Modes.
 
diff --git a/apps/tc/elpi/parser_addInstances.elpi b/apps/tc/elpi/parser_addInstances.elpi
index 386dbc766..0c0631c7a 100644
--- a/apps/tc/elpi/parser_addInstances.elpi
+++ b/apps/tc/elpi/parser_addInstances.elpi
@@ -1,6 +1,10 @@
 /* license: GNU Lesser General Public License Version 2.1 or later           */
 /* ------------------------------------------------------------------------- */
 
+accumulate base.
+accumulate tc_aux.
+accumulate compiler.
+
 kind enum type.
 type path  string -> string -> enum.
 type addInstPrio int -> string -> enum.
diff --git a/apps/tc/elpi/rewrite_forward.elpi b/apps/tc/elpi/rewrite_forward.elpi
index b602a9a13..fca7fc60e 100644
--- a/apps/tc/elpi/rewrite_forward.elpi
+++ b/apps/tc/elpi/rewrite_forward.elpi
@@ -1,6 +1,8 @@
 /* license: GNU Lesser General Public License Version 2.1 or later           */
 /* ------------------------------------------------------------------------- */
 
+accumulate base.
+
 pred forward i:term, o:term, o:list (pair (list term) term).
 
 % Auxiliary function for rewrite-forward
diff --git a/apps/tc/elpi/solver.elpi b/apps/tc/elpi/solver.elpi
index 8aeb3c19e..8c6453e49 100644
--- a/apps/tc/elpi/solver.elpi
+++ b/apps/tc/elpi/solver.elpi
@@ -1,8 +1,18 @@
 /* license: GNU Lesser General Public License Version 2.1 or later           */
 /* ------------------------------------------------------------------------- */
 
+accumulate base.
+
+pred time-solve i:prop.
+time-solve P :-
+  std.time P Time,
+  if (is-option-active oTC-time) (coq.say "[TC] Total resolution time is:" Time) true.
+
 msolve L N :- !,
-  coq.ltac.all (coq.ltac.open solve) {std.rev L} N.
+  time-solve (coq.ltac.all (coq.ltac.open solve-aux) {std.rev L} N).
+
+solve A L :- time-solve (solve-aux A L).
+
 
 pred build-context-clauses i:list prop, o:list prop.
 % Add the section's definition to the given context
@@ -20,48 +30,49 @@ tc-recursive-search Ty Sol :-
   std.time (coq.safe-dest-app Ty (global TC) TL',
     std.append TL' [Sol] TL,
     coq.elpi.predicate {gref->pred-name TC} TL Q, Q) Time,
-  if (is-option-active {oTC-resolution-time}) (coq.say "Instance search" Time) true.
+  if (is-option-active oTC-time-instance-search) (coq.say "[TC] Instance search time is:" Time) true.
 
 :if "solve-print-goal"
 solve (goal Ctx _ Ty _ _) _ :-
   coq.say "Ctx" Ctx "Ty" Ty, fail.
 
-% solve (goal C _ (prod N Ty F) S _ as _G) _L GL :- !,
+pred solve-aux i:goal, o:list sealed-goal.
+% solve-aux (goal C _ (prod N Ty F) S _ as _G) _L GL :- !,
 %   @pi-decl  N Ty x\
 %     declare-evar [decl x N Ty|C] (Raw x) (F x) (Sol x),
-%     solve (goal [decl x N Ty|C] (Raw x) (F x) (Sol x) []) _L GL,
+%     solve-aux (goal [decl x N Ty|C] (Raw x) (F x) (Sol x) []) _L GL,
 %     if (Sol x = app [HD, x]) (S = HD) (S = fun N Ty Sol).
-% solve (goal C _ (prod N Ty F) XX _ as G) _L GL :- !,
+% solve-aux (goal C _ (prod N Ty F) XX _ as G) _L GL :- !,
 %   % intros_if_needed Prod C [] 
 %   (@pi-decl  N Ty x\
 %     declare-evar [decl x N Ty|C] (Raw x) (F x) (Sol x),
-%     solve (goal [decl x N Ty|C] (Raw x) (F x) (Sol x) []) _L _,
+%     solve-aux (goal [decl x N Ty|C] (Raw x) (F x) (Sol x) []) _L _,
 %     coq.safe-dest-app (Sol x) Hd (Args x)),
 %     if (pi x\ last-no-error (Args x) x, std.drop-last 1 (Args x) NewArgs)
 %     (coq.mk-app Hd NewArgs Out, refine Out G GL) (
 %       % coq.say "Not eta" (Sol x) x (fun N Ty Sol),
 %       XX = (fun N Ty Sol)).
-% solve (goal C _ (prod N _ _ as P) _ A as G) _L GL :- !,
+% solve-aux (goal C _ (prod N _ _ as P) _ A as G) _L GL :- !,
 %   declare-evar C T P S',
 %   G' = (goal C T P S' A),
 %   refine (fun N _ _) G' GL1,
-%   coq.ltac.all (coq.ltac.open solve) GL1 _,
+%   coq.ltac.all (coq.ltac.open solve-aux) GL1 _,
 %   refine S' G GL.
-solve (goal C _ (prod N Ty F) _ _ as G) GL :- !,
+solve-aux (goal C _ (prod N Ty F) _ _ as G) GL :- !,
   (@pi-decl N Ty x\
     declare-evar [decl x N Ty|C] (Raw x) (F x) (Sol x),
-    solve (goal [decl x N Ty|C] (Raw x) (F x) (Sol x) []) _),
+    solve-aux (goal [decl x N Ty|C] (Raw x) (F x) (Sol x) []) _),
     if (pi x\ 
       % also check the head does not contain x
       coq.safe-dest-app (Sol x) Hd (Args x), 
       last-no-error (Args x) x, 
       std.drop-last 1 (Args x) NewArgs)
     (coq.mk-app Hd NewArgs Out, refine Out G GL1) (refine (fun N _ _) G GL1),
-    coq.ltac.all (coq.ltac.open solve) GL1 GL.
-% solve (goal _ _ (prod N _ _) _ _ as G) GL :- !,
+    coq.ltac.all (coq.ltac.open solve-aux) GL1 GL.
+% solve-aux (goal _ _ (prod N _ _) _ _ as G) GL :- !,
 %   refine (fun N _ _) G GL1,
-%   coq.ltac.all (coq.ltac.open solve) GL1 GL.
-solve (goal Ctx _ Ty Sol _ as G) GL :-
+%   coq.ltac.all (coq.ltac.open solve-aux) GL1 GL.
+solve-aux (goal Ctx _ Ty Sol _ as G) GL :-
   var Sol,
   build-context-clauses Ctx Clauses,
   % @redflags! coq.redflags.beta => coq.reduction.lazy.norm Ty Ty1,
@@ -71,10 +82,10 @@ solve (goal Ctx _ Ty Sol _ as G) GL :-
       % coq.say "Solution " X "end" X' "caio",
       % std.assert! (ground_term X') "solution not complete",
       % (pi F\ (copy (fun _ _ x\ (app [F, x])) F :- !)) => copy X X',
-      if (is-option-active {oTC-ignore-eta-reduction}) 
+      if (is-option-active oTC-ignore-eta-reduction) 
         (Proof' = Proof) (coq.reduction.eta-contract Proof Proof'),
       std.time (refine Proof' G GL) Refine-Time, 
-      if (is-option-active {oTC-time-refine}) (coq.say "Refine Time" Refine-Time) true;
+      if (is-option-active oTC-time-refine) (coq.say "[TC] Refine time is:" Refine-Time) true;
       coq.error "illtyped solution:" {coq.term->string Proof}
     ) 
     (GL = [seal G]).
diff --git a/apps/tc/elpi/tc_aux.elpi b/apps/tc/elpi/tc_aux.elpi
index 3cb72af47..dab16588d 100644
--- a/apps/tc/elpi/tc_aux.elpi
+++ b/apps/tc/elpi/tc_aux.elpi
@@ -1,10 +1,14 @@
 /* license: GNU Lesser General Public License Version 2.1 or later           */
 /* ------------------------------------------------------------------------- */
 
+accumulate base.
+
 % Contains the list of classes that
 % cannot be compiled
 
 % returns the TC from the type of an instance
+% TODO: This gould be replaced with an api 
+% coq.TC.get-class-of-inst i:gref, o:gref
 pred get-TC-of-inst-type i:term, o:gref.
 get-TC-of-inst-type (prod _ _ A) GR:-
   pi x\ get-TC-of-inst-type (A x) GR.
@@ -67,12 +71,15 @@ get-last (app L) R :-
 % TC preds are on the form tc-[PATH_TO_TC].tc-[TC-Name]
 pred gref->pred-name i:gref, o:string.
 gref->pred-name Gr S :-
-  if (is-option-active {oTC-clauseNameShortName})
+  if (is-option-active oTC-clauseNameShortName)
     (Path = "")
     (coq.gref->path Gr [Hd | Tl], 
       std.fold Tl Hd (x\acc\r\ r is acc ^ "." ^ x) Path', 
       Path is Path' ^ ".tc-"),
-  S is "tc-" ^ Path ^ {coq.gref->id Gr}.
+  % CAVEAT : Non-ascii caractars can't be part of a pred
+  %          name, we replace ö with o
+  rex.replace "ö" "o" {coq.gref->id Gr} GrStr,
+  S is "tc-" ^ Path ^ GrStr.
 
 pred no-backtrack i:list prop, o:list prop. 
 no-backtrack [] [].
@@ -90,23 +97,20 @@ make-tc _IsHead Ty Inst Hyp Clause :-
       (Hyp = [Hd]) (Clause = (Q :- Hd)) 
       (Clause = (Q :- Hyp)).
 
+pred unwrap-prio i:tc-priority, o:int.
+unwrap-prio (tc-priority-given Prio) Prio.
+unwrap-prio (tc-priority-computed Prio) Prio.
+
 % returns the priority of an instance from the gref of an instance
 pred get-inst-prio i:gref, o:int.
-get-inst-prio InstGr Prio :-
-  coq.env.typeof InstGr InstTy,
-  get-TC-of-inst-type InstTy TC,
-  find-opt {coq.TC.db-for TC} 
-    (x\ tc-instance InstGr (tc-priority-given Prio) = x ;
-        tc-instance InstGr (tc-priority-computed Prio) = x)
-      (some _), !.
-get-inst-prio _ 0.
-
-% TODO: @FissoreD improve this method complexity
+get-inst-prio InstGR Prio :-
+  coq.env.typeof InstGR InstTy,
+  get-TC-of-inst-type InstTy ClassGR,
+  unwrap-prio {coq.TC.get-inst-prio ClassGR InstGR} Prio.
+
 pred get-full-path i:gref, o:string.
-% :if "get-full-path"
 get-full-path Gr Res' :-
   coq.gref->string Gr Path,
   coq.env.current-section-path SectionPath,
   std.fold SectionPath "" (e\acc\r\ r is acc ^ "." ^ e) Res,
   Res' is Res ^ Path.
-% get-full-path _ _.
\ No newline at end of file
diff --git a/apps/tc/theories/add_commands.v b/apps/tc/theories/add_commands.v
index ac5bd8629..fa7a01e3f 100644
--- a/apps/tc/theories/add_commands.v
+++ b/apps/tc/theories/add_commands.v
@@ -3,18 +3,15 @@
 
 From elpi.apps Require Import db.
 
-From elpi.apps.tc Extra Dependency "base.elpi" as base.
+From elpi.apps.tc Extra Dependency "tc_aux.elpi" as tc_aux.
 From elpi.apps.tc Extra Dependency "compiler.elpi" as compiler.
 From elpi.apps.tc Extra Dependency "parser_addInstances.elpi" as parser_addInstances.
 From elpi.apps.tc Extra Dependency "solver.elpi" as solver.
-From elpi.apps.tc Extra Dependency "tc_aux.elpi" as tc_aux.
 From elpi.apps.tc Extra Dependency "create_tc_predicate.elpi" as create_tc_predicate.
 
 Elpi Command TC.AddAllInstances.
 Elpi Accumulate Db tc.db.
 Elpi Accumulate Db tc_options.db.
-Elpi Accumulate File base.
-Elpi Accumulate File tc_aux.
 Elpi Accumulate File compiler.
 Elpi Accumulate lp:{{  
   main L :- 
@@ -26,9 +23,6 @@ Elpi Typecheck.
 Elpi Command TC.AddInstances.
 Elpi Accumulate Db tc.db.
 Elpi Accumulate Db tc_options.db.
-Elpi Accumulate File base.
-Elpi Accumulate File tc_aux.
-Elpi Accumulate File compiler.
 Elpi Accumulate File parser_addInstances.
 Elpi Accumulate lp:{{
   main Arguments :- 
@@ -39,21 +33,18 @@ Elpi Typecheck.
 Elpi Command TC.AddAllClasses.
 Elpi Accumulate Db tc.db.
 Elpi Accumulate Db tc_options.db.
-Elpi Accumulate File base.
-Elpi Accumulate File tc_aux.
 Elpi Accumulate File create_tc_predicate.
 Elpi Accumulate lp:{{
-  main _ :-
-    coq.TC.db-tc TC,
-    std.forall TC (add-class-gr classic).
+  % Ignore is the list of classes we do not want to add
+  main IgnoreStr :-
+    std.map IgnoreStr (x\r\ sigma S\ str S = x, coq.locate S r) IgnoreGR,
+    std.forall {coq.TC.db-tc} (x\ if (std.mem IgnoreGR x) true (add-class-gr classic x)).
 }}.
 Elpi Typecheck.
 
 Elpi Command TC.AddClasses.
 Elpi Accumulate Db tc.db.
 Elpi Accumulate Db tc_options.db.
-Elpi Accumulate File base.
-Elpi Accumulate File tc_aux.
 Elpi Accumulate File create_tc_predicate.
 Elpi Accumulate lp:{{
   main L :-
@@ -67,7 +58,6 @@ Elpi Typecheck.
 Elpi Command TC.AddHook.
 Elpi Accumulate Db tc.db.
 Elpi Accumulate Db tc_options.db.
-Elpi Accumulate File base.
 Elpi Accumulate File tc_aux.
 Elpi Accumulate lp:{{
   pred addHook i:grafting, i:string. 
@@ -98,8 +88,6 @@ Elpi Typecheck.
 Elpi Command TC.Declare.
 Elpi Accumulate Db tc.db.
 Elpi Accumulate Db tc_options.db.
-Elpi Accumulate File base.
-Elpi Accumulate File tc_aux.
 Elpi Accumulate File create_tc_predicate.
 Elpi Accumulate lp:{{
   main [indt-decl D] :- declare-class D.
diff --git a/apps/tc/theories/db.v b/apps/tc/theories/db.v
index a51fd422c..7eb299707 100644
--- a/apps/tc/theories/db.v
+++ b/apps/tc/theories/db.v
@@ -3,6 +3,9 @@
 
 From elpi Require Import elpi.
 
+From elpi.apps.tc Extra Dependency "base.elpi".
+From elpi.apps.tc Extra Dependency "tc_aux.elpi".
+
 (* 
   tc_option.db contains the set of options used by the solver of tc. 
   all the options are set to false by default
@@ -11,14 +14,20 @@ Elpi Db tc_options.db lp:{{
   pred oTC-ignore-eta-reduction o:list string. 
   oTC-ignore-eta-reduction ["TC", "IgnoreEtaReduction"].
 
-  pred oTC-resolution-time o:list string. 
-  oTC-resolution-time ["TC", "ResolutionTime"].
+  % Time taken by only instance search (we time tc-recursive-search) 
+  pred oTC-time-instance-search o:list string. 
+  oTC-time-instance-search ["TC", "Time", "Instance", "Search"].
 
-  pred oTC-clauseNameShortName o:list string. 
-  oTC-clauseNameShortName ["TC", "NameShortPath"].
+  % Time taken by the whole search in tc
+  pred oTC-time o:list string.
+  oTC-time ["TC", "Time"].
 
+  % Time taken to refine the solution
   pred oTC-time-refine o:list string. 
-  oTC-time-refine ["TC", "TimeRefine"].
+  oTC-time-refine ["TC", "Time", "Refine"].
+
+  pred oTC-clauseNameShortName o:list string. 
+  oTC-clauseNameShortName ["TC", "NameShortPath"].
 
   pred oTC-debug o:list string.
   oTC-debug ["TC", "Debug"].
@@ -26,9 +35,16 @@ Elpi Db tc_options.db lp:{{
   pred oTC-use-pattern-fragment-compiler o:list string. 
   oTC-use-pattern-fragment-compiler ["TC", "CompilerWithPatternFragment"].
 
-  pred is-option-active i:list string.
-  is-option-active Opt :- 
-    coq.option.get Opt (coq.option.bool tt).
+  pred all-options o:list ((list string) -> prop).
+  all-options [
+    oTC-ignore-eta-reduction, oTC-time-refine, oTC-time,
+    oTC-clauseNameShortName, oTC-time-instance-search, oTC-debug, 
+    oTC-use-pattern-fragment-compiler
+  ].
+
+  pred is-option-active i:(list string -> prop).
+  is-option-active Opt :-
+    Opt X, coq.option.get X (coq.option.bool tt).
 }}.
 
 Elpi Db tc.db lp:{{
diff --git a/apps/tc/theories/tc.v b/apps/tc/theories/tc.v
index 65f422da9..3b255f23d 100644
--- a/apps/tc/theories/tc.v
+++ b/apps/tc/theories/tc.v
@@ -3,11 +3,9 @@
 
 Declare ML Module "coq-elpi-tc.plugin".
 
-From elpi.apps.tc Extra Dependency "base.elpi" as base.
+From elpi.apps.tc Extra Dependency "tc_aux.elpi" as tc_aux.
 From elpi.apps.tc Extra Dependency "compiler.elpi" as compiler.
-From elpi.apps.tc Extra Dependency "parser_addInstances.elpi" as parser_addInstances.
 From elpi.apps.tc Extra Dependency "solver.elpi" as solver.
-From elpi.apps.tc Extra Dependency "tc_aux.elpi" as tc_aux.
 From elpi.apps.tc Extra Dependency "create_tc_predicate.elpi" as create_tc_predicate.
 
 From elpi.apps Require Import db.
@@ -38,18 +36,14 @@ Elpi Typecheck.
 Elpi Tactic TC.Solver.
 Elpi Accumulate Db tc.db.
 Elpi Accumulate Db tc_options.db.
-Elpi Accumulate File base.
-Elpi Accumulate File tc_aux.
 Elpi Accumulate File compiler.
 Elpi Accumulate File create_tc_predicate.
 Elpi Accumulate File solver.
 Elpi Query lp:{{
   sigma Options\ 
-    Options = [oTC-ignore-eta-reduction, oTC-resolution-time, 
-      oTC-clauseNameShortName, oTC-time-refine, oTC-debug, 
-      oTC-use-pattern-fragment-compiler],
-    std.forall Options (x\ sigma Args\ x Args, 
-      coq.option.add Args (coq.option.bool ff) ff).
+    all-options Options,
+    std.forall Options (x\ sigma L\ x L, 
+      coq.option.add L (coq.option.bool ff) ff).
 }}.
 Elpi Typecheck.
 
@@ -65,8 +59,6 @@ Elpi Query lp:{{
 Elpi Command TC.Compiler.
 Elpi Accumulate Db tc.db.
 Elpi Accumulate Db tc_options.db.
-Elpi Accumulate File base.
-Elpi Accumulate File tc_aux.
 Elpi Accumulate File create_tc_predicate.
 Elpi Accumulate File compiler.
 Elpi Accumulate lp:{{
@@ -90,7 +82,6 @@ Elpi Typecheck.
 Elpi Command TC.Set_deterministic.
 Elpi Accumulate Db tc.db.
 Elpi Accumulate Db tc_options.db.
-Elpi Accumulate File base.
 Elpi Accumulate File tc_aux.
 Elpi Accumulate lp:{{
   main [str ClassStr] :- 
diff --git a/coq-builtin.elpi b/coq-builtin.elpi
index 7e2efa79f..2e9741208 100644
--- a/coq-builtin.elpi
+++ b/coq-builtin.elpi
@@ -1154,6 +1154,10 @@ external pred coq.TC.db-tc o:list gref.
 % Instances are in their precedence order.
 external pred coq.TC.db-for i:gref, o:list tc-instance.
 
+% [coq.TC.get-inst-prio ClassGR InstGR InstPrio] reads the priority of an
+% instance
+external pred coq.TC.get-inst-prio i:gref, i:gref, o:tc-priority.
+
 % [coq.TC.class? GR] checks if GR is a class
 external pred coq.TC.class? i:gref.
 
diff --git a/elpi-builtin.elpi b/elpi-builtin.elpi
index 4c6705dd6..0c1dd7f4d 100644
--- a/elpi-builtin.elpi
+++ b/elpi-builtin.elpi
@@ -537,6 +537,10 @@ pred fold i:list B, i:A, i:(B -> A -> A -> prop), o:A.
 fold [] A _ A.
 fold [X|XS] A F R :- F X A A1, fold XS A1 F R.
 
+pred fold-right i:list B, i:A, i:(B -> A -> A -> prop), o:A.
+fold-right [] A _ A.
+fold-right [X|XS] A F R :- fold-right XS A F A', F X A' R.
+
 pred fold2 i:list C, i:list B, i:A, i:(C -> B -> A -> A -> prop), o:A.
 fold2 [] [_|_] _ _ _ :- fatal-error "fold2 on lists of different length".
 fold2 [_|_] [] _ _ _ :- fatal-error "fold2 on lists of different length".
diff --git a/src/coq_elpi_builtins.ml b/src/coq_elpi_builtins.ml
index 324203a49..bfb59afa6 100644
--- a/src/coq_elpi_builtins.ml
+++ b/src/coq_elpi_builtins.ml
@@ -485,8 +485,8 @@ let tc_instance = let open Conv in let open API.AlgebraicData in declare {
       M (fun ~ok ~ko { implementation; priority } -> ok implementation priority));
 ]} |> CConv.(!<)
 
-let get_instance_prio gr env sigma (info : 'a Typeclasses.hint_info_gen) : tc_priority =
-  match info.hint_priority with
+let get_instance_prio gr env sigma (hint_priority : int option) : tc_priority =
+  match hint_priority with
   | Some p -> UserGiven p
   | None -> 
     let rec nb_hyp sigma c = match EConstr.kind sigma c with
@@ -511,20 +511,50 @@ let get_instance_prio gr env sigma (info : 'a Typeclasses.hint_info_gen) : tc_pr
     let hyps = nb_hyp sigma' cty in
     Computed (hyps + nmiss)
 
-let get_instances (env: Environ.env) (emap: Evd.evar_map) tc : type_class_instance list = 
+(* TODO: this algorithm is quite inefficient since we have not yet the
+         possibility to get the implementation of an instance from its gref in
+         coq. Currently we have to get all the instances of the tc and the find
+         its implementation.
+*)
+let get_isntances_of_tc env sigma (tc : GlobRef.t) = 
+  let inst_of_tc = (* contains all the instances of a type class *)
+    Typeclasses.instances_exn env sigma tc |>
+    List.fold_left (fun m i -> GlobRef.Map.add i.Typeclasses.is_impl i m) GlobRef.Map.empty in
+  inst_of_tc
+
+let get_instance env sigma inst_of_tc instance : type_class_instance =
+  let instances_grefs2istance inst_gr : type_class_instance = 
+    let open Typeclasses in 
+    let user_hint_prio = 
+      (* Note: in general we deal with an instance I of a type class. Here we
+               look if the user has given a priority to I. However, external
+               hints are not in the inst_of_tc (the Not_found exception) *)
+      try (GlobRef.Map.find inst_gr inst_of_tc).is_info.hint_priority 
+      with Not_found -> None in
+    let priority = get_instance_prio inst_gr env sigma user_hint_prio in 
+    { implementation = inst_gr; priority } 
+  in
+  instances_grefs2istance instance
+
+let warning_tc_hints = CWarnings.create ~name:"TC.hints" ~category:elpi_cat Pp.str
+
+
+let get_instances (env: Environ.env) (sigma: Evd.evar_map) tc : type_class_instance list = 
   let hint_db = Hints.searchtable_map "typeclass_instances" in 
   let secvars : Names.Id.Pred.t = Names.Id.Pred.full in 
   let full_hints = Hints.Hint_db.map_all ~secvars:secvars tc hint_db in 
-  let hint_asts = List.map Hints.FullHint.repr full_hints in 
-  let hints = List.filter_map (function
-    | Hints.Res_pf a -> Some a 
-    | ERes_pf a -> Some a
-    | Extern (a, b) -> None 
-    | Give_exact a -> Some a
-    | Res_pf_THEN_trivial_fail e -> Some e
-    | Unfold_nth e -> None) hint_asts in 
-  let sigma, _ = 
-    let env = Global.env () in Evd.(from_env env, env) in 
+  (* let hint_asts = List.map Hints.FullHint.repr full_hints in  *)
+  let hints = List.filter_map (fun (e : Hints.FullHint.t) -> match Hints.FullHint.repr e with
+    | Hints.Res_pf a | ERes_pf a | Give_exact a -> Some a (* Respectively Hint Apply | EApply | Exact *)
+    | Extern _ -> 
+      warning_tc_hints (Printf.sprintf "There is an hint extern in the typeclass db: \n%s" (Pp.string_of_ppcmds @@ Hints.FullHint.print env sigma e)); 
+      None
+    | Res_pf_THEN_trivial_fail _ -> (* Hint Immediate *)
+      warning_tc_hints (Printf.sprintf "There is an hint immediate in the typeclass db: \n%s" (Pp.string_of_ppcmds @@ Hints.FullHint.print env sigma e)); 
+      None
+    | Unfold_nth _ -> 
+      warning_tc_hints (Printf.sprintf "There is an hint unfold in the typeclass db: \n%s" (Pp.string_of_ppcmds @@ Hints.FullHint.print env sigma e)); 
+      None) full_hints in 
   let constrs = List.map (fun a -> Hints.hint_as_term a |> snd) hints in 
   (* Printer.pr_global tc |> Pp.string_of_ppcmds |> Printf.printf "%s\n"; *)
   let instances_grefs = List.filter_map (fun e ->
@@ -532,16 +562,9 @@ let get_instances (env: Environ.env) (emap: Evd.evar_map) tc : type_class_instan
     | Constr.Ind (a, _) -> Some (Names.GlobRef.IndRef a)
     | Constr.Const (a, _) -> Some (Names.GlobRef.ConstRef a)
     | Constr.Construct (a, _) -> Some (Names.GlobRef.ConstructRef a)
-    | _ -> None) constrs in 
-  let inst_of_tc =
-    Typeclasses.instances_exn env emap tc |>
-    List.fold_left (fun m i -> GlobRef.Map.add i.Typeclasses.is_impl i m) GlobRef.Map.empty in
-  let instances_grefs2istance x = 
-    let open Typeclasses in 
-    let inst = GlobRef.Map.find x inst_of_tc in
-    let priority = get_instance_prio x env sigma inst.is_info in 
-    { implementation = x; priority } in 
-  List.map instances_grefs2istance instances_grefs
+    | _ -> None) constrs in
+  let isnt_of_tc = get_isntances_of_tc env sigma tc in
+  List.map (get_instance env sigma isnt_of_tc) instances_grefs
 
 type scope = ExecutionSite | CurrentModule | Library
 
@@ -2830,6 +2853,18 @@ Supported attributes:
   (fun gr _ ~depth { env } _ state -> !: (get_instances env (get_sigma state) gr))),
   DocAbove);
 
+  MLCode(Pred("coq.TC.get-inst-prio", 
+    In(gref, "ClassGR",
+    In(gref, "InstGR",
+    Out(tc_priority, "InstPrio",
+    Read (global, "reads the priority of an instance")))),
+    (fun class_gr inst_gr _ ~depth { env } _ state ->
+      let sigma = get_sigma state in
+      let inst_of_tc = get_isntances_of_tc env sigma class_gr in
+      let {priority} = get_instance env sigma inst_of_tc inst_gr in 
+      !: priority)),
+  DocAbove);
+
   MLCode(Pred("coq.TC.class?",
     In(gref, "GR",
     Easy "checks if GR is a class"),