diff --git a/.gitignore b/.gitignore
index a8d712e50..c9d2ab4b9 100644
--- a/.gitignore
+++ b/.gitignore
@@ -46,4 +46,5 @@ META
 *.cache
 
 apps/coercion/src/coq_elpi_coercion_hook.ml
-.filestoinstall
\ No newline at end of file
+.filestoinstall
+apps/tc/src/coq_elpi_tc_hook.ml
diff --git a/apps/tc/_CoqProject b/apps/tc/_CoqProject
index 1e009a732..50c6dbae3 100644
--- a/apps/tc/_CoqProject
+++ b/apps/tc/_CoqProject
@@ -5,7 +5,9 @@
 
 -R theories   elpi.apps
 -R elpi       elpi.apps.tc
+-R tests    elpi.apps.tc.tests
 
+src/coq_elpi_tc_register.ml
 src/coq_elpi_tc_hook.mlg
 src/coq_elpi_class_tactics_hacked.ml
 src/elpi_tc_plugin.mlpack
diff --git a/apps/tc/_CoqProject.test b/apps/tc/_CoqProject.test
index 5eab1487e..905583fe0 100644
--- a/apps/tc/_CoqProject.test
+++ b/apps/tc/_CoqProject.test
@@ -7,6 +7,8 @@
 -R tests    elpi.apps.tc.tests
 -I src
 
+tests/auto_compile.v
+
 tests/premisesSort/sortCode.v
 tests/premisesSort/sort1.v
 # tests/premisesSort/sort2.v
@@ -20,16 +22,15 @@ tests/importOrder/sameOrderCommand.v
 tests/importOrder/f1.v
 tests/importOrder/f2a.v
 tests/importOrder/f2b.v
-# tests/importOrder/f3a.v
-# tests/importOrder/f3b.v
-# tests/importOrder/f3c.v
-# tests/importOrder/f3d.v
-# tests/importOrder/f3e.v
-# tests/importOrder/f3f.v
-# tests/importOrder/f3g.v
+tests/importOrder/f3a.v
+tests/importOrder/f3b.v
+tests/importOrder/f3c.v
+tests/importOrder/f3d.v
+tests/importOrder/f3e.v
+tests/importOrder/f3f.v
+tests/importOrder/f3g.v
 
 tests/nobacktrack.v
-tests/removeEta.v
 tests/patternFragment.v
 tests/contextDeepHierarchy.v
 tests/mode_no_repetion.v
diff --git a/apps/tc/elpi/compiler.elpi b/apps/tc/elpi/compiler.elpi
index 5302000a2..c1155c94a 100644
--- a/apps/tc/elpi/compiler.elpi
+++ b/apps/tc/elpi/compiler.elpi
@@ -145,18 +145,32 @@ has-context-deps GR :-
   coq.env.dependencies GR _ Deps, 
   std.exists SectionVars (x\ coq.gref.set.mem (const x) Deps).
 
-% [add-inst->db IgnoreClassDepL Inst] add the Inst to
-% the database except those depending on at least one 
-% inside IgnoreClassDepL
 pred is-local.
 is-local :- std.mem {attributes} (attribute "local" _).
 
-pred make-inst-graft i:gref, i:bool, o:grafting.
-make-inst-graft Inst _NoPremises (after Grafting) :- 
-  RawGrafting is int_to_string {get-inst-prio Inst},
-  % if (NoPremises = tt) (Grafting = RawGrafting) (Grafting is RawGrafting ^ "_complex").
-  Grafting = RawGrafting.
+pred get-locality i:string, o:list prop.
+get-locality "Local" [@local!].
+get-locality _ [@local!] :- coq.env.current-section-path [_ | _].
+get-locality "Global" [@global!].
+get-locality "Export" [].
 
+pred add-inst i:gref, i:gref, i:string, i:int.
+add-inst Inst TC Locality Prio :-
+  coq.env.current-section-path SectionPath,
+  compile Inst _ TC Clause, 
+  % TODO: a clause is flexible if an instance is polimorphic (pglobal)
+  not (var Clause),
+  if (Prio = -1) (get-inst-prio Inst Prio1) (Prio1 = Prio),
+  Graft is after (int_to_string Prio1),
+  get-full-path Inst ClauseName,
+  get-locality Locality LocalityProp,
+  LocalityProp => (add-tc-db ClauseName Graft Clause, add-tc-db _ Graft (instance SectionPath Inst TC)).
+add-inst Inst _ _ _ :- 
+  coq.warning "Not-added" "TC_solver" "Warning : Cannot compile " Inst "since it is pglobal".
+
+% [add-inst->db IgnoreClassDepL ForceAdd Inst] add the Inst to
+% the database except those depending on at least one 
+% inside IgnoreClassDepL
 pred add-inst->db i:list gref, i:bool, i:gref.
 :name "add-inst->db:start"
 add-inst->db IgnoreClassDepL ForceAdd Inst :-
@@ -166,10 +180,10 @@ add-inst->db IgnoreClassDepL ForceAdd Inst :-
   if ((ForceAdd = tt; not (instance _ Inst _)), 
     not (std.exists Dep (std.mem IgnoreClassDepL)), not (banned Inst)) 
   (
-    compile Inst IsLeaf TC-of-Inst Clause, 
+    compile Inst _IsLeaf TC-of-Inst Clause, 
     % TODO: a clause is flexible if an instance is polimorphic (pglobal)
     not (var Clause),
-    make-inst-graft Inst IsLeaf Graft,
+    Graft is after (int_to_string {get-inst-prio Inst}),
     get-full-path Inst ClauseName,
     if (is-local) (Visibility = [@local!])
       (if (has-context-deps Inst) 
diff --git a/apps/tc/elpi/solver.elpi b/apps/tc/elpi/solver.elpi
index 64f7f9bf0..c08472d4f 100644
--- a/apps/tc/elpi/solver.elpi
+++ b/apps/tc/elpi/solver.elpi
@@ -25,7 +25,7 @@ build-context-clauses Ctx Clauses :-
 
 pred tc i:term, o:term.
 tc Ty Sol :- 
-  Ty = app [global TC | TL'],
+  coq.safe-dest-app Ty (global TC) TL',
   std.append TL' [Sol] TL,
   % replace-with-alias T T' A, !, 
   % A = tt, tc Gref T' Sol.
diff --git a/apps/tc/elpi/tc_aux.elpi b/apps/tc/elpi/tc_aux.elpi
index b4d3ffac8..abea7e6f0 100644
--- a/apps/tc/elpi/tc_aux.elpi
+++ b/apps/tc/elpi/tc_aux.elpi
@@ -97,7 +97,7 @@ no-backtrack [X | XS] [std.do! [X | XS']] :- !, no-backtrack XS XS'.
 
 pred make-tc i:prop, i:term, i:term, i:list prop, o:prop.
 make-tc _IsHead Ty Inst Hyp Clause :-
-  app [global TC | TL] = Ty,
+  coq.safe-dest-app Ty (global TC) TL,
   gref->string-no-path TC TC_Str,
   std.append TL [Inst] Args, 
   coq.elpi.predicate TC_Str Args Q,
@@ -106,22 +106,15 @@ make-tc _IsHead Ty Inst Hyp Clause :-
       (Hyp = [Hd]) (Clause = (Q :- Hd)) 
       (Clause = (Q :- Hyp)).
 
-
-pred get-inst-prio-coq i:term, i:list term, o:int.
-get-inst-prio-coq (prod _ _ A) L Prio :-
-  pi x\ get-inst-prio-coq (A x) [x | L] Prio.
-get-inst-prio-coq (app _ as App) L Prio :-
-  std.fold L 0 (T\acc\r\ if (not(occurs T App)) (r is acc + 1) (r = acc)) Prio.
-get-inst-prio-coq A _ _ :- coq.error "Invalid case for" A.
-
 % 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 Prio' = x) (some _), !,
-  if (Prio' = 0) (get-inst-prio-coq InstTy [] Prio) (Prio = Prio').
+    (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
diff --git a/apps/tc/src/coq_elpi_class_tactics_hacked.ml b/apps/tc/src/coq_elpi_class_tactics_hacked.ml
index ea19c0e63..a4b59f9b0 100644
--- a/apps/tc/src/coq_elpi_class_tactics_hacked.ml
+++ b/apps/tc/src/coq_elpi_class_tactics_hacked.ml
@@ -27,14 +27,6 @@ open Elpi
 open Elpi_plugin
 open Coq_elpi_utils
 
-let handle_event = function
- | Classes.Event.NewClass _ -> assert false
- | Classes.Event.NewInstance _ -> assert false
-
-let this_observer =
-  Classes.register_observer ~name:"elpi.tc" handle_event
-
-
 module NamedDecl = Context.Named.Declaration
 
 (** Hint database named "typeclass_instances", created in prelude *)
@@ -1181,7 +1173,6 @@ let elpi_solver = Summary.ref ~name:"tc_takeover" None
 
 let takeover action =
   let open Names.GlobRef in
-  Classes.activate_observer this_observer;
   match !elpi_solver, action with
   | _, Set(solver,mode) ->
     elpi_solver := Some (mode,solver)
diff --git a/apps/tc/src/coq_elpi_tc_hook.ml b/apps/tc/src/coq_elpi_tc_hook.ml
deleted file mode 100644
index a4dc4187e..000000000
--- a/apps/tc/src/coq_elpi_tc_hook.ml
+++ /dev/null
@@ -1,93 +0,0 @@
-let _ = Mltop.add_known_module "coq-elpi-tc.plugin"
-
-# 3 "src/coq_elpi_tc_hook.mlg"
- 
-open Stdarg
-open Elpi_plugin
-open Coq_elpi_arg_syntax
-open Coq_elpi_class_tactics_hacked
-
-module M = Coq_elpi_vernacular
-
-
-
-let () = Vernacextend.static_vernac_extend ~plugin:(Some "coq-elpi-tc.plugin") ~command:"ElpiTypeclasses" ~classifier:(fun _ -> Vernacextend.classify_as_sideeff) ?entry:None 
-         [(Vernacextend.TyML (false, Vernacextend.TyTerminal ("Elpi", 
-                                     Vernacextend.TyTerminal ("Override", 
-                                     Vernacextend.TyTerminal ("TC", Vernacextend.TyNonTerminal (
-                                                                    Extend.TUentry (Genarg.get_arg_tag wit_qualified_name), 
-                                                                    Vernacextend.TyTerminal ("All", 
-                                                                    Vernacextend.TyNil))))), 
-         (let coqpp_body p
-         atts = Vernacextend.vtdefault (fun () -> 
-# 15 "src/coq_elpi_tc_hook.mlg"
-                                                                                   
-     let () = ignore_unknown_attributes atts in
-     takeover false [] (snd p) 
-                ) in fun p
-         ?loc ~atts () -> coqpp_body p (Attributes.parse any_attribute atts)), None));
-         (Vernacextend.TyML (false, Vernacextend.TyTerminal ("Elpi", 
-                                    Vernacextend.TyTerminal ("Override", 
-                                    Vernacextend.TyTerminal ("TC", Vernacextend.TyNonTerminal (
-                                                                   Extend.TUentry (Genarg.get_arg_tag wit_qualified_name), 
-                                                                   Vernacextend.TyTerminal ("None", 
-                                                                   Vernacextend.TyNil))))), 
-         (let coqpp_body p
-         atts = Vernacextend.vtdefault (fun () -> 
-# 18 "src/coq_elpi_tc_hook.mlg"
-                                                                                    
-     let () = ignore_unknown_attributes atts in
-     takeover true [] (snd p) 
-                ) in fun p
-         ?loc ~atts () -> coqpp_body p (Attributes.parse any_attribute atts)), None));
-         (Vernacextend.TyML (false, Vernacextend.TyTerminal ("Elpi", 
-                                    Vernacextend.TyTerminal ("Override", 
-                                    Vernacextend.TyTerminal ("TC", Vernacextend.TyNonTerminal (
-                                                                   Extend.TUentry (Genarg.get_arg_tag wit_qualified_name), 
-                                                                   Vernacextend.TyTerminal ("Only", 
-                                                                   Vernacextend.TyNonTerminal (
-                                                                   Extend.TUlist1 (
-                                                                   Extend.TUentry (Genarg.get_arg_tag wit_reference)), 
-                                                                   Vernacextend.TyNil)))))), 
-         (let coqpp_body p cs
-         atts = Vernacextend.vtdefault (fun () -> 
-# 23 "src/coq_elpi_tc_hook.mlg"
-                                                                                                          
-     let () = ignore_unknown_attributes atts in
-     takeover false cs (snd p) 
-                ) in fun p
-         cs ?loc ~atts () -> coqpp_body p cs
-         (Attributes.parse any_attribute atts)), None));
-         (Vernacextend.TyML (false, Vernacextend.TyTerminal ("Elpi", 
-                                    Vernacextend.TyTerminal ("Override", 
-                                    Vernacextend.TyTerminal ("TC", Vernacextend.TyTerminal ("+", 
-                                                                   Vernacextend.TyNonTerminal (
-                                                                   Extend.TUlist0 (
-                                                                   Extend.TUentry (Genarg.get_arg_tag wit_reference)), 
-                                                                   Vernacextend.TyNil))))), 
-         (let coqpp_body cs
-         atts = Vernacextend.vtdefault (fun () -> 
-# 26 "src/coq_elpi_tc_hook.mlg"
-                                                                                  
-     let () = ignore_unknown_attributes atts in
-     takeover_add cs 
-                ) in fun cs
-         ?loc ~atts () -> coqpp_body cs
-         (Attributes.parse any_attribute atts)), None));
-         (Vernacextend.TyML (false, Vernacextend.TyTerminal ("Elpi", 
-                                    Vernacextend.TyTerminal ("Override", 
-                                    Vernacextend.TyTerminal ("TC", Vernacextend.TyTerminal ("-", 
-                                                                   Vernacextend.TyNonTerminal (
-                                                                   Extend.TUlist0 (
-                                                                   Extend.TUentry (Genarg.get_arg_tag wit_reference)), 
-                                                                   Vernacextend.TyNil))))), 
-         (let coqpp_body cs
-         atts = Vernacextend.vtdefault (fun () -> 
-# 29 "src/coq_elpi_tc_hook.mlg"
-                                                                                  
-     let () = ignore_unknown_attributes atts in
-     takeover_rm cs 
-                ) in fun cs
-         ?loc ~atts () -> coqpp_body cs
-         (Attributes.parse any_attribute atts)), None))]
-
diff --git a/apps/tc/src/coq_elpi_tc_hook.mlg b/apps/tc/src/coq_elpi_tc_hook.mlg
index 09ec0faae..cc621e5c4 100644
--- a/apps/tc/src/coq_elpi_tc_hook.mlg
+++ b/apps/tc/src/coq_elpi_tc_hook.mlg
@@ -4,6 +4,7 @@ DECLARE PLUGIN "coq-elpi-tc.plugin"
 open Stdarg
 open Elpi_plugin
 open Coq_elpi_arg_syntax
+open Coq_elpi_tc_register
 open Coq_elpi_class_tactics_hacked
 
 }
@@ -28,4 +29,8 @@ VERNAC COMMAND EXTEND ElpiTypeclasses CLASSIFIED AS SIDEFF
      let () = ignore_unknown_attributes atts in
      takeover_rm cs }
 
+| #[ atts = any_attribute ] [ "Elpi" "Override" "TC_Register" qualified_name(p) ] -> {
+     let () = ignore_unknown_attributes atts in
+     register_observer (fst p, snd p, atts) }
+
 END
\ No newline at end of file
diff --git a/apps/tc/src/coq_elpi_tc_register.ml b/apps/tc/src/coq_elpi_tc_register.ml
new file mode 100644
index 000000000..651270a29
--- /dev/null
+++ b/apps/tc/src/coq_elpi_tc_register.ml
@@ -0,0 +1,70 @@
+open Elpi_plugin
+open Classes
+open Coq_elpi_arg_HOAS
+
+type qualified_name = Coq_elpi_utils.qualified_name
+
+type loc_name_atts = (Loc.t * qualified_name * Attributes.vernac_flags)
+  
+let gref2elpi_term (gref: Names.GlobRef.t) : Cmd.raw = 
+  let gref_2_string gref = Pp.string_of_ppcmds (Names.GlobRef.print gref) in
+  let normalize_string s = 
+    String.split_on_char '.' s |> List.rev |> List.hd |>
+    String.split_on_char ',' |> List.hd  in
+  Cmd.Term (CAst.make @@ Constrexpr.CRef(
+    Libnames.qualid_of_string @@ normalize_string @@ gref_2_string gref,None))
+
+let observer_class (x : Typeclasses.typeclass) : Coq_elpi_arg_HOAS.Cmd.raw list = 
+  [gref2elpi_term x.cl_impl]
+
+(* 
+  The elpi arguments passed to the elpi program are [Inst, TC, Locality, Prio] where: 
+  - Inst     : is the elpi Term for the current instance 
+  - TC       : is the elpi Term for the type classes implemented by Inst
+  - Locality : is the elpi String [Local|Global] depending on the locality of Inst 
+  - Prio     : is the elpi Int X representing the priority of the instance
+               in particular if the priority is defined by the user, X is that priority
+               otherwise, X is -1
+*)
+let observer_instance ({locality; instance; info; class_name} : instance) : Coq_elpi_arg_HOAS.Cmd.raw list = 
+  let locality2elpi_string loc = 
+    let hint2string = function 
+    | Hints.Local -> "Local"
+    | Export -> "Export"
+    | SuperGlobal -> "Global" in
+    Cmd.String (hint2string loc) in 
+  let prio2elpi_int (prio: Typeclasses.hint_info) = 
+    Cmd.Int (Option.default (-1) prio.hint_priority) in 
+  [
+    gref2elpi_term instance; 
+    gref2elpi_term class_name;
+    locality2elpi_string locality;
+    prio2elpi_int info
+  ]
+
+let inObservation =
+  Libobject.declare_object @@
+    Libobject.local_object "TC_HACK_OBSERVER2"
+      ~cache:(fun (run,inst) -> run @@ observer_instance inst)
+      ~discharge:(fun (_,inst as x) -> if inst.locality = Hints.Local then None else Some x)
+
+let observer_evt ((loc, name, atts) : loc_name_atts) (x : Event.t) = 
+  let open Coq_elpi_vernacular in
+  let run_program e = run_program loc name ~atts e in 
+  match x with  
+  | Event.NewClass cl -> run_program @@ observer_class cl
+  | Event.NewInstance inst -> Lib.add_leaf (inObservation (run_program,inst))
+
+let inTakeover =
+  let cache (loc, name, atts) = 
+    let observer1 = Classes.register_observer 
+                    ~name:(String.concat "." name) 
+                    (observer_evt (loc, name, atts))
+    in
+    Classes.activate_observer observer1
+  in
+  Libobject.(declare_object 
+    (superglobal_object_nodischarge "TC_HACK_OBSERVER" ~cache ~subst:None))
+
+let register_observer (x : loc_name_atts) = 
+  Lib.add_leaf (inTakeover x)
\ No newline at end of file
diff --git a/apps/tc/src/elpi_tc_plugin.mlpack b/apps/tc/src/elpi_tc_plugin.mlpack
index 8aed0b167..1e62bcd54 100644
--- a/apps/tc/src/elpi_tc_plugin.mlpack
+++ b/apps/tc/src/elpi_tc_plugin.mlpack
@@ -1,2 +1,3 @@
+Coq_elpi_tc_register
 Coq_elpi_class_tactics_hacked
 Coq_elpi_tc_hook
\ No newline at end of file
diff --git a/apps/tc/tests/auto_compile.v b/apps/tc/tests/auto_compile.v
new file mode 100644
index 000000000..3ea473912
--- /dev/null
+++ b/apps/tc/tests/auto_compile.v
@@ -0,0 +1,79 @@
+From elpi.apps Require Import tc.
+
+Elpi Override TC_Register auto_compiler.
+Elpi Override TC TC_solver All.
+
+Require Import Bool.
+
+(* TODO: How to add the #[deterministic] pragma in front of the class? *)
+(* #[deterministic] Class A (T : Type) := {succ : T -> T}. *)
+Class A (T : Type) := {succ : T -> T}.
+#[local] Instance B : A nat := {succ n := S n}.
+Instance C : A bool := {succ b := negb b}.
+Instance Prod (X Y: Type) `(A X, A Y) : A (X * Y) := 
+  {succ b := match b with (a, b) => (succ a, succ b) end}.
+
+Elpi Accumulate TC_solver lp:{{
+  :after "firstHook"
+  solve _ _ :- coq.say "Solving in ELPI!", fail.
+}}.
+
+Goal A (nat * (nat * bool)). apply _. Qed.
+
+Module M.
+  Class B (T : nat).
+  Section A. 
+    Instance X : B 1. Qed.
+    Goal B 1. apply _. Qed.
+
+    Global Instance Y : B 2. Qed.
+    Goal B 2. apply _. Qed.
+  End A.
+  Goal B 1. Proof. Fail apply _. Abort.
+  Goal B 2. Proof. apply _. Qed.
+
+  Section B.
+    Variable V : nat.
+    Global Instance Z : `(B 0) -> B V. Qed.
+    Global Instance W : B 0. Qed.
+  End B.
+
+  Goal B 0. apply _. Qed.
+  Goal B 10. apply _. Qed.
+End M.
+
+Goal M.B 1. apply M.X. Qed.
+Goal M.B 0. apply _. Qed.
+Goal M.B 10. apply _. Qed.
+
+(* 
+  TODO: @gares @FissoreD we have an unwanted warning:
+  constant tc-elpi.apps.tc.tests.auto_compile.M.tc-B has no declared type
+  since the considered instances come from a module.
+*)
+Elpi Query TC_solver lp:{{
+  % Small test for instance order
+  sigma I L\
+  std.findall (instance _ _ _) I,
+  std.map-filter I (x\y\ x = instance _ y {{:gref M.B}}) 
+    [{{:gref M.W}}, {{:gref M.Y}}, {{:gref M.Z}}].
+}}.
+
+Module S.
+  Class Cl (i: nat).
+  #[local] Instance Cl1 : Cl 1. Qed.
+  #[global] Instance Cl2 : Cl 2. Qed.
+  #[export] Instance Cl3 : Cl 3. Qed.
+End S.
+
+Elpi Override TC TC_solver None.
+Goal S.Cl 1 /\ S.Cl 2 /\ S.Cl 3.
+Proof. 
+  split. all:cycle 1.
+  split.
+  apply _.
+  Fail apply _.
+  Import S.
+  apply _.
+  Fail apply _.
+Abort.
\ No newline at end of file
diff --git a/apps/tc/tests/eqSimpl.v b/apps/tc/tests/eqSimpl.v
index 07948357e..ff08779e1 100644
--- a/apps/tc/tests/eqSimpl.v
+++ b/apps/tc/tests/eqSimpl.v
@@ -12,7 +12,6 @@ Elpi AddInstances Eqb.
 Elpi Override TC TC_solver All.
 Fail Check (fun n m : _ => eqb n m).
 
-Elpi Trace Browser.
 Goal (tt, (tt, true)) == (tt, (tt, true)) = true.
   easy.
 Qed.
diff --git a/apps/tc/tests/eqSimplDef.v b/apps/tc/tests/eqSimplDef.v
index c2e1854d8..916cde199 100644
--- a/apps/tc/tests/eqSimplDef.v
+++ b/apps/tc/tests/eqSimplDef.v
@@ -8,13 +8,4 @@ Notation " x == y " := (eqb x y) (no associativity, at level 70).
 Global Instance eqU : Eqb unit := { eqb x y := true }.
 Global Instance eqB : Eqb bool := { eqb x y := if x then y else negb y }.
 Global Instance eqP {A B} `{Eqb A} `{Eqb B} : Eqb (A * B) := { 
-  eqb x y := (fst x == fst y) && (snd x == snd y) }.
-(* Global Instance eqN : Eqb nat := { 
-  eqb := fix add (a: nat) b := match a, b with 
-  | 0, 0 => true 
-  | S a, S b => add a b 
-  | _, _ => false
-  end }.
-
-  
-Check (forall n, n + n == 2 * n = true). *)
\ No newline at end of file
+  eqb x y := (fst x == fst y) && (snd x == snd y) }.
\ No newline at end of file
diff --git a/apps/tc/tests/importOrder/f1.v b/apps/tc/tests/importOrder/f1.v
index a2b17d269..70c4c1c1c 100644
--- a/apps/tc/tests/importOrder/f1.v
+++ b/apps/tc/tests/importOrder/f1.v
@@ -2,6 +2,4 @@ From elpi.apps.tc.tests.importOrder Require Export sameOrderCommand.
 
 Class A (T : Set) := f : T -> T.
 
-Elpi AddClasses A.
-
 Elpi SameOrderImport.
\ No newline at end of file
diff --git a/apps/tc/tests/importOrder/f2a.v b/apps/tc/tests/importOrder/f2a.v
index 0fcf326c3..9c3839098 100644
--- a/apps/tc/tests/importOrder/f2a.v
+++ b/apps/tc/tests/importOrder/f2a.v
@@ -7,5 +7,4 @@ Global Instance f2ab : A nat := {f x := x}.
 Global Instance f2ac : A nat := {f x := x}.
 Global Instance f2ad : A nat := {f x := x}.
 
-Elpi AddInstances A.
-(* Elpi SameOrderImport. *)
\ No newline at end of file
+Elpi SameOrderImport.
\ No newline at end of file
diff --git a/apps/tc/tests/importOrder/f2b.v b/apps/tc/tests/importOrder/f2b.v
index 2f87a80aa..b7ec3d03e 100644
--- a/apps/tc/tests/importOrder/f2b.v
+++ b/apps/tc/tests/importOrder/f2b.v
@@ -5,5 +5,5 @@ Global Instance f2bb : A nat := {f x := x}.
 Global Instance f2bc : A nat := {f x := x}.
 Global Instance f2bd : A nat := {f x := x}.
 
-Elpi AddInstances A.
+
 (* Elpi SameOrderImport. *)
diff --git a/apps/tc/tests/importOrder/f3a.v b/apps/tc/tests/importOrder/f3a.v
index c32eac7c1..58d5444fd 100644
--- a/apps/tc/tests/importOrder/f3a.v
+++ b/apps/tc/tests/importOrder/f3a.v
@@ -1,7 +1,4 @@
 From elpi.apps.tc.tests.importOrder Require Import f2a.
 From elpi.apps.tc.tests.importOrder Require Import f2b.
-(* Elpi AddAllInstances. *)
-Print HintDb typeclass_instances.
 
-Elpi Print TC_solver "tests/f3a".
 Elpi SameOrderImport.
diff --git a/apps/tc/tests/importOrder/f3b.v b/apps/tc/tests/importOrder/f3b.v
index dce7ecc47..41f84e7aa 100644
--- a/apps/tc/tests/importOrder/f3b.v
+++ b/apps/tc/tests/importOrder/f3b.v
@@ -1,7 +1,4 @@
 From elpi.apps.tc.tests.importOrder Require Import f2b.
 From elpi.apps.tc.tests.importOrder Require Import f2a.
-(* Elpi AddAllInstances. *)
-Print HintDb typeclass_instances.
 
-Elpi Print TC_solver "tests/f3b".
 Elpi SameOrderImport.
\ No newline at end of file
diff --git a/apps/tc/tests/importOrder/f3c.v b/apps/tc/tests/importOrder/f3c.v
index 1027dcd20..2c94dfcb2 100644
--- a/apps/tc/tests/importOrder/f3c.v
+++ b/apps/tc/tests/importOrder/f3c.v
@@ -3,24 +3,27 @@ From elpi.apps.tc.tests.importOrder Require Export f1.
 Global Instance f3a : A nat := {f x := x}.
 Global Instance f3b : A nat := {f x := x}.
 Global Instance f3c : A nat := {f x := x}.
-Elpi AddAllInstances.
+
 Elpi SameOrderImport.
 
-Section S1.
-  Global Instance f3d : A nat := {f x := x}.
+Section S1. Variable X : Type.
+  Local Instance f3d : A nat := {f x := x}.
   Global Instance f3e : A nat := {f x := x}.
   Global Instance f3f : A nat := {f x := x}.
-  Elpi AddAllInstances.
+
   Elpi SameOrderImport.
-MySectionEnd.
+End S1.
+
+
 Elpi SameOrderImport.
 
 Section S2.
   Context (T : Set).
   Global Instance f3g : A T := {f x := x}.
-  Elpi AddAllInstances.
+
   Elpi SameOrderImport.
-MySectionEnd.
+End S2.
+
 Elpi SameOrderImport.
 
 Section S3.
@@ -32,8 +35,7 @@ Section S3.
   Global Instance f3g3 : A (T: Set) := {f x := x}.
   Global Instance f3g4 : A (T: Set) | 10 := {f x := x}.
 
-  Elpi AddAllInstances.
   Elpi SameOrderImport.
-MySectionEnd.
+End S3.
 
 Elpi SameOrderImport.
\ No newline at end of file
diff --git a/apps/tc/tests/importOrder/f3d.v b/apps/tc/tests/importOrder/f3d.v
index 4b1a9bdcb..84c4b3b45 100644
--- a/apps/tc/tests/importOrder/f3d.v
+++ b/apps/tc/tests/importOrder/f3d.v
@@ -3,7 +3,7 @@ From elpi.apps.tc.tests.importOrder Require Import f2b.
 Elpi SameOrderImport.
 
 Global Instance f3a' T1 T2 `(A T1, A T2) : A (T1 * T2) := {f x := x}.
-Elpi AddInstances A.
+
 
 Elpi SameOrderImport.
 Module M4'.
@@ -11,21 +11,22 @@ Module M4'.
   Elpi SameOrderImport.
 
   Global Instance f3a : A nat := {f x := x}.
-  Elpi AddInstances f3a.
+  
 
-  Section S1.
+  Section S1. Variable X : Type.
     Global Instance f3b : A nat := {f x := x}.
-    Elpi AddInstances f3b.
-    Section S1'.
+    
+    Section S1'. Variable Y : Type.
       Global Instance f3c : A nat := {f x := x}.
-      Elpi AddInstances f3c.
-    MySectionEnd.
-  MySectionEnd.
+      
+    End S1'.
+  End S1.
 
   Elpi SameOrderImport.
 
-  Section S2.
+  Section S2. Variable X : Type.
     Global Instance f3h T1 T2 `(A T1, A T2) : A (T1 * T2) := {f x := x}.
-    Elpi AddInstances f3h.
-  MySectionEnd.
-End M4'.
\ No newline at end of file
+  End S2.
+End M4'.
+
+Elpi SameOrderImport.
diff --git a/apps/tc/tests/importOrder/f3e.v b/apps/tc/tests/importOrder/f3e.v
index fbffe2a68..0de8467ce 100644
--- a/apps/tc/tests/importOrder/f3e.v
+++ b/apps/tc/tests/importOrder/f3e.v
@@ -1,25 +1,24 @@
 From elpi.apps.tc.tests.importOrder Require Export f1.
 From elpi.apps.tc.tests.importOrder Require Import f2b.
+From elpi.apps.tc.tests.importOrder Require Import f2a.
 
 Global Instance f3a' T1 T2 `(A T1, A T2) : A (T1 * T2) := {f x := x}.
-Elpi AddAllInstances.
+
 Elpi SameOrderImport.
 Module M4'.
-  From elpi.apps.tc.tests.importOrder Require Import f2a.
-
   Global Instance f3a : A nat := {f x := x}.
 
-  Section S1.
+  Section S1. Variable X : Type.
     Global Instance f3b : A nat := {f x := x}.
-    Section S1'.
+    Section S1'. Variable Y : Type.
       Global Instance f3c : A nat := {f x := x}.
-    MySectionEnd.
-  MySectionEnd.
+    End S1'.
+  End S1.
 
-  Section S2.
-    Global Instance f3h T1 T2 `(A T1, A T2) : A (T1 * T2) := {f x := x}.
-  MySectionEnd.
+  Section S2. Variable X : Type.
+    Global Instance f3h T1 T2 `(A T1, A T2) : A (T1 * T2) | 100 := {f x := x}.
+  End S2.
 End M4'.
 
-Elpi AddAllInstances. 
+
 Elpi SameOrderImport.
\ No newline at end of file
diff --git a/apps/tc/tests/importOrder/f3f.v b/apps/tc/tests/importOrder/f3f.v
index d183876c1..2b0db45ee 100644
--- a/apps/tc/tests/importOrder/f3f.v
+++ b/apps/tc/tests/importOrder/f3f.v
@@ -3,15 +3,15 @@ From elpi.apps.tc.tests.importOrder Require Import f1.
 Section S1.
   Context (T : Set).
   Global Instance f3a : A T := {f x := x}.
-  Elpi AddInstances f3a.
+  
   Elpi SameOrderImport.
 
   Section S2.
     Context (T1 : Set).
     Global Instance f3b : A T1 := {f x := x}.
-    Elpi AddInstances f3b.
-  MySectionEnd.
+    
+  End S2.
   
   Elpi SameOrderImport.
-MySectionEnd.
+End S1.
 Elpi SameOrderImport.
\ No newline at end of file
diff --git a/apps/tc/tests/importOrder/f3g.v b/apps/tc/tests/importOrder/f3g.v
index 1650e3416..608efd7f1 100644
--- a/apps/tc/tests/importOrder/f3g.v
+++ b/apps/tc/tests/importOrder/f3g.v
@@ -2,10 +2,8 @@ From elpi.apps.tc.tests.importOrder Require Export f1.
 
 Module M8.
   Class Classe (A: Type) (B: Type).
-  Elpi AddClasses Classe.
 
   Global Instance I (a b c d: Type): Classe a a -> Classe b c. Admitted.
 
-  Elpi AddAllInstances.
   Elpi SameOrderImport.
 End M8.
diff --git a/apps/tc/tests/importOrder/f4.v b/apps/tc/tests/importOrder/f4.v
index 62681ca25..0d73340cd 100644
--- a/apps/tc/tests/importOrder/f4.v
+++ b/apps/tc/tests/importOrder/f4.v
@@ -1 +1,8 @@
-From elpi.apps.tc.tests.importOrder Require Import f3f.
\ No newline at end of file
+From elpi.apps.tc.tests.importOrder Require Import f3f.
+From elpi.apps.tc.tests.importOrder Require Import f2a.
+From elpi.apps.tc.tests.importOrder Require Import f2b.
+From elpi.apps.tc.tests.importOrder Require Import f3c.
+From elpi.apps.tc.tests.importOrder Require Import f3d.
+From elpi.apps.tc.tests.importOrder Require Import f3g.
+
+Elpi SameOrderImport.
\ No newline at end of file
diff --git a/apps/tc/tests/importOrder/sameOrderCommand.v b/apps/tc/tests/importOrder/sameOrderCommand.v
index 1e7980554..fb4770c1f 100644
--- a/apps/tc/tests/importOrder/sameOrderCommand.v
+++ b/apps/tc/tests/importOrder/sameOrderCommand.v
@@ -1,14 +1,13 @@
-From elpi Require Export tc.
+From elpi.apps Require Export tc.
+
+From elpi.apps.tc Extra Dependency "base.elpi" as base.
+From elpi.apps.tc.tests.importOrder Extra Dependency "tc_same_order.elpi" as tc_same_order.
 
 Elpi Command SameOrderImport.
 Elpi Accumulate Db tc.db.
-Elpi Accumulate lp:{{
-  main _ :-
-    std.findall (instance _ _ _) RulesInst,
-    coq.TC.db DB_tc-inst,
-    std.map RulesInst (x\inst\ instance _Path inst _TC = x) RulesElpi,
-    std.map DB_tc-inst (x\inst\ tc-instance inst _ = x) RulesCoq,
-    if (RulesElpi = RulesCoq) true (
-      coq.error "Error in import order\n" 
-      "Expected :" RulesCoq "\nFound   :" RulesElpi).
-}}.
\ No newline at end of file
+Elpi Accumulate File base.
+Elpi Accumulate File tc_same_order.
+Elpi Typecheck.
+
+Elpi Override TC_Register auto_compiler.
+Elpi Override TC TC_solver All.
\ No newline at end of file
diff --git a/apps/tc/tests/importOrder/tc_same_order.elpi b/apps/tc/tests/importOrder/tc_same_order.elpi
new file mode 100644
index 000000000..4d4607123
--- /dev/null
+++ b/apps/tc/tests/importOrder/tc_same_order.elpi
@@ -0,0 +1,24 @@
+% [Typeclass, Coq Instances, Elpi Instances]
+% the instances of the given typeclass should be in the same order as Coq
+pred correct_instance_order_aux i:gref, i:(list tc-instance), i:(list gref).
+:name "tc-correct-instance-order-aux"
+correct_instance_order_aux _ [] [].
+correct_instance_order_aux TC [tc-instance I1 _ | TL1] [I1 | TL2] :-
+  correct_instance_order_aux TC TL1 TL2. 
+
+% [Typeclasses of Coq, Elpi Instances]
+pred correct_instance_order i:(list gref), i:(list prop).
+:name "tc-correct-instance-order"
+correct_instance_order [] _.
+correct_instance_order [TC | TL] ElpiInst :-
+  coq.TC.db-for TC CoqInst,
+  std.map-filter ElpiInst (x\r\ sigma I\ x = instance _ I TC, r = I) ElpiInstTC,
+  if (correct_instance_order_aux TC CoqInst ElpiInstTC) 
+    (correct_instance_order TL ElpiInst)
+    (coq.error "Error in import order\n" 
+    "Expected :" CoqInst "\nFound   :" ElpiInstTC).
+
+:name "tc-same-order-main"
+main _ :-
+  std.findall (instance _ _ _) ElpiInst,
+  correct_instance_order {coq.TC.db-tc} ElpiInst.
\ No newline at end of file
diff --git a/apps/tc/tests/patternFragmentBug.v b/apps/tc/tests/patternFragmentBug.v
index 8570fd7fc..31174df32 100644
--- a/apps/tc/tests/patternFragmentBug.v
+++ b/apps/tc/tests/patternFragmentBug.v
@@ -48,7 +48,7 @@ Unset Typeclass Resolution For Conversion.
 Goal  Z bool.
 intros.
 (* TODO: here Elpi Trace Fails... *)
-Elpi Trace Browser.
+(* Elpi Trace Browser. *)
 
   (* Elpi Override TC TC_solver Only Z. *)
   (* Elpi Override TC - Z. *)
diff --git a/apps/tc/tests/section_in_out.v b/apps/tc/tests/section_in_out.v
index e643d2d09..fa484adbe 100644
--- a/apps/tc/tests/section_in_out.v
+++ b/apps/tc/tests/section_in_out.v
@@ -1,13 +1,16 @@
 From elpi.apps Require Import tc.
 From elpi.apps.tc Extra Dependency "base.elpi" as base.
 
+Elpi Accumulate tc.db lp:{{
+  pred origial_tc o:int. 
+}}.
+
 Elpi Command len_test.
 Elpi Accumulate Db tc.db.
 Elpi Accumulate File base.
 Elpi Accumulate lp:{{
   % contains the number of instances that are not 
   % imported from other files
-  pred origial_tc o:int. 
   main [int Len] :-
     std.findall (instance _ _ _) Insts,
     std.map Insts (x\r\ instance _ r _ = x) R,
@@ -17,7 +20,6 @@ Elpi Accumulate lp:{{
     std.forall R (x\ sigma L\
       std.assert! (count R x L, L = 1) "Duplicates in instances"). 
 }}.
-(* Elpi Typecheck. *)
 
 Elpi Query TC_solver lp:{{
   std.findall (instance _ _ _) Rules,
diff --git a/apps/tc/tests/test.v b/apps/tc/tests/test.v
index e15c7603f..d95a858ce 100644
--- a/apps/tc/tests/test.v
+++ b/apps/tc/tests/test.v
@@ -1,6 +1,7 @@
 From elpi.apps.tc.tests Require Import stdppInj.
 Elpi TC_solver. Set TimeRefine. Set TimeTC. Set Debug "elpitime". 
 Elpi Accumulate TC_solver lp:{{
+  shorten tc-elpi.apps.tc.tests.stdppInj.{tc-Inj}.
   :after "firstHook"
   tc-Inj A B RA RB {{@compose lp:A lp:A lp:A lp:FL lp:FL}} Sol :- !, 
     tc-Inj A B RA RB FL Sol1, 
diff --git a/apps/tc/theories/tc.v b/apps/tc/theories/tc.v
index 157eb4f91..473945124 100644
--- a/apps/tc/theories/tc.v
+++ b/apps/tc/theories/tc.v
@@ -61,8 +61,8 @@ Elpi Accumulate lp:{{
 
 Elpi Command MySectionEnd.
 Elpi Accumulate Db tc.db.
-Elpi Accumulate File tc_aux.
 Elpi Accumulate File base.
+Elpi Accumulate File tc_aux.
 Elpi Accumulate File modes.
 Elpi Accumulate File compiler.
 Elpi Accumulate lp:{{
@@ -75,8 +75,8 @@ Elpi Accumulate lp:{{
 
 Elpi Command AddAllInstances.
 Elpi Accumulate Db tc.db.
-Elpi Accumulate File tc_aux.
 Elpi Accumulate File base.
+Elpi Accumulate File tc_aux.
 Elpi Accumulate File modes.
 Elpi Accumulate File compiler.
 Elpi Accumulate lp:{{  
@@ -156,8 +156,8 @@ Elpi Accumulate lp:{{
 
 Elpi Tactic TC_solver.
 Elpi Accumulate Db tc.db.
-Elpi Accumulate File rforward.
 Elpi Accumulate File base.
+Elpi Accumulate File rforward.
 Elpi Accumulate File tc_aux.
 Elpi Accumulate File modes.
 Elpi Accumulate File alias.
@@ -210,3 +210,18 @@ Elpi Export MySectionEnd.
 
 Elpi AddAllClasses.
 Elpi AddAllInstances.
+
+Elpi Command auto_compiler.
+Elpi Accumulate File base.
+Elpi Accumulate File tc_aux.
+Elpi Accumulate Db tc.db.
+Elpi Accumulate File create_tc_predicate.
+Elpi Accumulate File compiler.
+Elpi Accumulate lp:{{
+  main [trm (global Inst), trm (global TC), str Locality, int Prio] :- 
+    add-inst Inst TC Locality Prio.
+
+  main [trm (global GR)] :- 
+    add-class-gr classic GR.
+}}.
+Elpi Typecheck.
\ No newline at end of file
diff --git a/coq-builtin.elpi b/coq-builtin.elpi
index fa4f798d4..da1556585 100644
--- a/coq-builtin.elpi
+++ b/coq-builtin.elpi
@@ -1125,9 +1125,14 @@ external pred coq.CS.db-for i:gref, i:cs-pattern, o:list cs-instance.
 % [coq.TC.declare-class GR] Declare GR as a type class
 external pred coq.TC.declare-class i:gref.
 
+% Type class instance priority
+kind tc-priority type.
+type tc-priority-given int -> tc-priority. % User given priority
+type tc-priority-computed int -> tc-priority. % Coq computed priority
+
 % Type class instance with priority
 kind tc-instance type.
-type tc-instance gref -> int -> tc-instance.
+type tc-instance gref -> tc-priority -> tc-instance.
 
 % [coq.TC.declare-instance GR Priority] Declare GR as a Global type class
 % instance with Priority.
@@ -1141,7 +1146,8 @@ external pred coq.TC.db o:list tc-instance.
 % [coq.TC.db-tc TypeClasses] reads all type classes
 external pred coq.TC.db-tc o:list gref.
 
-% [coq.TC.db-for GR Db] reads all instances of the given class GR
+% [coq.TC.db-for GR InstanceList] reads all instances of the given class GR.
+% Instances are in their precedence order.
 external pred coq.TC.db-for i:gref, o:list tc-instance.
 
 % [coq.TC.class? GR] checks if GR is a class
diff --git a/src/coq_elpi_builtins.ml b/src/coq_elpi_builtins.ml
index ebb75198c..259af19df 100644
--- a/src/coq_elpi_builtins.ml
+++ b/src/coq_elpi_builtins.ml
@@ -442,17 +442,95 @@ let cs_instance = let open Conv in let open API.AlgebraicData in let open Struct
   ]
 } |> CConv.(!<)
 
-let tc_instance = let open Conv in let open API.AlgebraicData in let open Typeclasses in declare {
+
+type tc_priority = Computed of int | UserGiven of int
+
+let tc_priority = let open Conv in let open API.AlgebraicData in declare {
+  ty = TyName "tc-priority";
+  doc = "Type class instance priority";
+  pp = (fun fmt _ -> Format.fprintf fmt "<todo>");
+  constructors = [
+    K("tc-priority-given","User given priority",A(int,N),
+      B (fun i -> UserGiven i),
+      M (fun ~ok ~ko -> function UserGiven i -> ok i | _ -> ko ()));
+    K("tc-priority-computed","Coq computed priority", A(int,N),
+      B (fun i -> Computed i),
+      M (fun ~ok ~ko -> function Computed i -> ok i | _ -> ko ()));
+]} |> CConv.(!<)
+
+type type_class_instance = {
+  implementation : GlobRef.t;
+  priority : tc_priority;
+}
+
+let tc_instance = let open Conv in let open API.AlgebraicData in declare {
   ty = TyName "tc-instance";
   doc = "Type class instance with priority";
   pp = (fun fmt _ -> Format.fprintf fmt "<todo>");
   constructors = [
-    K("tc-instance","",A(gref,A(int,N)),
-      B (fun g p -> nYI "lp2instance"),
-      M (fun ~ok ~ko i ->
-          ok (instance_impl i) (Option.default 0 (hint_priority i))));
+    K("tc-instance","",A(gref,A(tc_priority,N)),
+      B (fun implementation priority -> { implementation; priority }),
+      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
+  | Some p -> UserGiven p
+  | None -> 
+    let rec nb_hyp sigma c = match EConstr.kind sigma c with
+    | Prod(_,_,c2) -> if EConstr.Vars.noccurn sigma 1 c2 then 1+(nb_hyp sigma c2) else nb_hyp sigma c2
+    | _ -> 0 in
+    let merge_context_set_opt sigma ctx = 
+      match ctx with
+      | None -> sigma
+      | Some ctx -> Evd.merge_context_set Evd.univ_flexible sigma ctx
+    in 
+    let fresh_global_or_constr env sigma = 
+        let (c, ctx) = UnivGen.fresh_global_instance env gr in
+        let ctx = if Environ.is_polymorphic env gr then Some ctx else None in
+        (EConstr.of_constr c, ctx) in
+    let c, ctx = fresh_global_or_constr env sigma in
+    let cty = Retyping.get_type_of env sigma c in
+    let cty = Reductionops.nf_betaiota env sigma cty in
+    let sigma' = merge_context_set_opt sigma ctx in
+    let ce = Clenv.mk_clenv_from env sigma' (c,cty) in
+    let miss = Clenv.clenv_missing ce in
+    let nmiss = List.length miss in
+    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 = 
+  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 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 ->
+    match EConstr.kind sigma e with 
+    | 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
+
 type scope = ExecutionSite | CurrentModule | Library
 
 let scope = let open Conv in let open API.AlgebraicData in declare {
@@ -1235,8 +1313,6 @@ let eta_contract env sigma t =
     map env t
 
 
-
-
 (*****************************************************************************)
 (*****************************************************************************)
 (*****************************************************************************)
@@ -2688,6 +2764,7 @@ Supported attributes:
      state, (), []))),
   DocAbove);
 
+  MLData tc_priority;
   MLData tc_instance;
  
   MLCode(Pred("coq.TC.declare-instance",
@@ -2706,8 +2783,12 @@ Supported attributes:
 
   MLCode(Pred("coq.TC.db",
     Out(list tc_instance, "Instances",
-    Easy "reads all type class instances"),
-  (fun _ ~depth -> !: (Typeclasses.all_instances ()))),
+    Read(global, "reads all type class instances")),
+  (fun _ ~depth { env } _ state ->
+    let sigma = get_sigma state in
+    let x = Typeclasses.typeclasses () in 
+    let classes = List.map (fun x -> x.Typeclasses.cl_impl) x in
+    !: (classes |> List.map (get_instances env sigma) |> List.concat))),
   DocAbove);
 
   MLCode(Pred("coq.TC.db-tc",
@@ -2719,12 +2800,11 @@ Supported attributes:
     l))),
   DocAbove);
 
-  MLCode(Pred("coq.TC.db-for",
+  MLCode(Pred("coq.TC.db-for", 
     In(gref, "GR",
-    Out(list tc_instance, "Db",
-    Read(global,"reads all instances of the given class GR"))),
-  (fun gr _ ~depth { env } _ state ->
-    !: (Typeclasses.instances_exn env (get_sigma state) gr))),
+    Out(list tc_instance,  "InstanceList",
+    Read (global, "reads all instances of the given class GR. Instances are in their precedence order."))),
+  (fun gr _ ~depth { env } _ state -> !: (get_instances env (get_sigma state) gr))),
   DocAbove);
 
   MLCode(Pred("coq.TC.class?",