diff --git a/apps/tc/README.md b/apps/tc/README.md
index 571aa29d5..a478429ff 100644
--- a/apps/tc/README.md
+++ b/apps/tc/README.md
@@ -109,14 +109,14 @@ In this implementation, the elpi rule for the instance `a3` is:
 
 ```elpi 
   tc-A {{3}} {{a3 lp:A lp:B lp:C}} :-
-    do-once (tc-NoBacktrack A B), 
+    once (tc-NoBacktrack A B), 
     tc-A A C.
 ```
 
-The predicate `do-once i:prop` has 
+The predicate `once i:prop` has 
 
 ```prolog
-do-once P :- P, !.
+once P :- P, !.
 ```
 
 as implementation. The cut (`!`) operator is in charge to avoid backtracking on 
diff --git a/apps/tc/elpi/WIP/deactivate_evar.elpi b/apps/tc/elpi/WIP/deactivate_evar.elpi
deleted file mode 100644
index a16001875..000000000
--- a/apps/tc/elpi/WIP/deactivate_evar.elpi
+++ /dev/null
@@ -1,27 +0,0 @@
-/*
-when solving a goal in tc, we want to trigger the declared evar only after
-the proof search. This means that, while the search is performed, we do not
-risk to assign too early incorrect types (for example with wrong universes).
-The evar typechecking is triggered after the search, just before refining the
-proof with the original goal.
-We use the guard declare-evars-now that to trigger the constraints to reproduce
-this behavior. 
-*/
-% pred declare-evar-later i:list prop, i:term, i:term, i:term.
-% pred declare-evars-now.
-
-% constraint declare-evar-later declare-evars-now {
-%    rule declare-evars-now \ (declare-evar-later Ctx RawEv Ty Ev) <=> (declare-evars-now, Ctx => evar RawEv Ty Ev).
-%    rule \ declare-evars-now.
-% }
-
-% declare-evars-now :-
-%   declare_constraint declare-evars-now [_].
-
-% We want to deactivate the evar declaration if coming from the
-% original goal (the original type class problem to be solved)
-% :before "default-declare-evar"
-% :name "tc-solver-declare-evar"
-% declare-evar Ctx X Ty E :- !,
-%   declare_constraint (declare-evar-later Ctx X Ty E) [_].
-
diff --git a/apps/tc/elpi/WIP/force_llam.elpi b/apps/tc/elpi/WIP/force_llam.elpi
deleted file mode 100644
index d89f2a239..000000000
--- a/apps/tc/elpi/WIP/force_llam.elpi
+++ /dev/null
@@ -1,131 +0,0 @@
-% This is an effort for forcing llam links when used as input variables
-% in a premise call. However, this brings several issues to find
-% the right variable to activate the right link.s
-namespace force-llam {
-  pred is-uvar-destruct i:term, o:term.
-  is-uvar-destruct T R :- name T Hd _, name-pair R Hd _, !.
-  is-uvar-destruct T T :- is-uvar T.
-
-  % At compile time, given a premise p with a flexible argument X.
-  % If X is expected to be in input mode, we add the auxiliary clause 
-  % `solve-llam-t X`, so that, if any suspended
-  % llam link on X exists, then it is forced before solving p 
-  pred modes i:list string, i:list term, o:list prop.
-  modes ["o"] [] [] :- !.
-  modes ["+" | Ms] [X | Xs] [P | Ps] :- is-uvar-destruct X R, !, 
-    P = tc.link.solve-llam-t R, modes Ms Xs Ps.
-  modes ["!" | Ms] [X | Xs] [P | Ps] :- is-uvar-destruct X R, !, 
-    P = tc.link.solve-llam-t R, modes Ms Xs Ps.
-  modes [_ | Ms] [_ | Xs] Ps :- 
-    modes Ms Xs Ps.
-
-  % The following rule represents a try to force llam links when input of
-  % of other premises. 
-  compile-conclusion ff Goal Proof HOPremisesIn HOPremisesOut Premises Clause :-
-    coq.safe-dest-app Goal Class Args,
-    tc.get-mode {tc.get-TC-of-inst-type Class} Modes,
-    force-llam.modes Modes Args ForceLlam,
-    tc.make-tc Goal Proof Premises ff Clause1, 
-    Prems = [HOPremisesIn, ForceLlam, [Clause1], HOPremisesOut],
-    std.flatten Prems AllPremises,
-    Clause = do AllPremises.
-
-  %                            Scope        Var     Args       Rhs
-  pred progress-llam-refine i:list term, i:term, i:list term, o:term.
-  progress-llam-refine S V [A|As] R :- name A, not (std.mem! S A), !,
-    % prune (V' A) [A|S],
-    eta V (fun _ _ (x\ V' x)),
-    progress-llam-refine [A|S] (V' A) As R.
-  progress-llam-refine _ V [] V.
-  progress-llam-refine _ V As (app [V|As]).
-
-  pred split-pf i:list term, i:list term, o:list term, o:list term.
-  split-pf [] _ [] [] :- !.
-  split-pf [X|Xs] Old [X|Ys] L :- name X, not (std.mem! Old X), !, split-pf Xs [X|Old] Ys L.
-  split-pf Xs _ [] Xs.
-
-  pred lam->fun i:term, i:list term, i:any.
-  lam->fun T [] R :- !, std.unsafe-cast R R', copy T T', R' = T'.
-  lam->fun Hd [H|L] R :- !,
-    pi x\ (copy H x :- !) => lam->fun Hd L (R' x),
-    std.unsafe-cast R Rx, Rx = R'.
-
-  pred unify-align i:term, i:term, i:list term, i:list term.
-  unify-align (app L) Hd PF NPF :-
-    Len is {std.length L} - {std.length NPF}, Len >= 0,
-    std.split-at Len L L' NPF,
-    Z = app L',
-    coq.mk-app Z NPF TT,
-    lam->fun TT {std.append PF NPF} Hd.
-
-  pred unify-const i:term, i:term, i:list term.
-  unify-const N R [] :- !, copy N X, R = X.
-  unify-const N R [A|As] :- not found.aux, A == N, !,
-    pi x\ found.aux => (copy N x :- !) => unify-const N (R' x) As,
-    std.unsafe-cast R Rx, Rx = R'.
-  unify-const N R [_|As] :- 
-    pi x\ unify-const N (R' x) As,
-    std.unsafe-cast R Rx, Rx = R'.
-
-  pred unify-heuristics i:term, i:term.
-  unify-heuristics A T :- tc.unify-eq A T.
-  % unify-heuristics (app _ as A) (fun _ _ B) :- !,
-  %   coq.error "A",
-  %   eta-expand A (fun _ _ A'), pi x\ unify-heuristics (A' x) (B x).
-  % unify-heuristics (app _ as A) B :- var B Hd Tl, !,
-  %   split-pf Tl [] PF NPF, 
-  %   unify-align A Hd PF NPF.
-  % unify-heuristics A B :- name A, var B Hd Tl, !, % TODO: also const
-  %   unify-const A Hd Tl.
-  % unify-heuristics (app L) (app[X|L']) :-
-  %   var X, !,
-  %   Len is {std.length L} - {std.length L'}, Len > 0,
-  %   std.split-at Len L Hd L',
-  %   if (Hd = [X]) true (X = app Hd).
-  % unify-heuristics (app L) (app L') :-
-  %   std.forall2 L L' unify-heuristics. 
-  % % The following rule leaves elpi uvars outside PF in coq
-  % % unify-heuristics A B :- A = B.
-  % % The following seems to solve the problem of the previous rule
-  % % TODO: I don't understand why the following rule cant be written as:
-  % % unify-heuristics A B :- var B Hb Lb, A = app[Hb|Lb] 
-  % % without breaking test CoqUvar2
-  % unify-heuristics (uvar Ha []) (uvar Hb Lb) :- !,
-  %     Ha = app[Hb|Lb].
-  % unify-heuristics (fun _ _ Bo) (uvar Hb_ Lb1) :- not (distinct_names Lb1), !,
-  %   Lb1 = [_ | Lb],
-  %   std.spy-do![prune Z Lb,
-  %   % std.unsafe-cast Hb Hb1,
-  %   (pi x\ unify-heuristics (Bo x) Z),
-  %   Hb_ = 
-  %   coq.error "TODO" Z].
-  % unify-heuristics A B :- A = B.
-
-  pred llam-aux i:term, i:term.
-  llam-aux A (uvar _ S as T) :- distinct_names S, !, A = T. % Here, both A and T are in PF
-  llam-aux A (uvar _ _ as T) :- !, A = T.
-  llam-aux A (app [H|L] as T) :- var A, var H, !, get-vars T Vars, declare_constraint (llam A (app [H|L])) [_,A|Vars].
-  llam-aux A (app [H|L] as T) :- var H, !, get-vars T Vars, declare_constraint (llam A (app [H|L])) [_|Vars].
-  llam-aux A (app [H|L]) :- coq.mk-app H L T, !, unify-heuristics A T.
-
-  llam L (app [H|As]) :- var H _ S, !,
-    progress-llam-refine S H As Rhs,
-    llam-aux L Rhs.
-  llam L Rhs :- llam-aux L Rhs.
-
-  pred solve-llam-t-cond i:term, i:term.
-  :name "solve-llam-t-cond"
-  solve-llam-t-cond (uvar A _) (app [uvar B _ | _]) :- A = B.
-
-  % Aims to force a llam link suspended on the given variable
-  pred solve-llam-t o:term.
-  solve-llam-t X :- var X, !, declare_constraint (solve-llam-t X) [X].
-  solve-llam-t _.
-
-  constraint solve-llam solve-llam-t llam {
-    rule \ (solve-llam-t X) (llam A B) | (solve-llam-t-cond X B) <=> (unify-heuristics A B).
-    rule solve-llam \ (llam A B) <=> (unify-heuristics A B).
-    rule \ solve-llam.
-  }
-}
-
diff --git a/apps/tc/elpi/WIP/modes.elpi b/apps/tc/elpi/WIP/modes.elpi
deleted file mode 100644
index a7f1d58fc..000000000
--- a/apps/tc/elpi/WIP/modes.elpi
+++ /dev/null
@@ -1,44 +0,0 @@
-/* license: GNU Lesser General Public License Version 2.1 or later           */
-/* ------------------------------------------------------------------------- */
-
-% pred make-modes-cl i:gref, i:list term, i:term, i:list (list hint-mode), i:list (list term), o:prop.
-% make-modes-cl T V (prod _ _ X) HintModes L (pi x\ C x):-
-%   std.map HintModes (x\r\ [r|_] = x) FST,
-%   std.map HintModes (x\r\ [_|r] = x) LAST,
-%   pi x\ sigma NewL\
-%     std.map2 L FST (l\m\r\ if (m = mode-input) (r = [x | l]) (r = l)) NewL,
-%     make-modes-cl T [x | V] (X x) LAST NewL (C x).
-% make-modes-cl T V _ _ L Clause :-
-%   Ty = {coq.mk-app (global T) {std.rev V}},
-%   Clause = (pi s\ tc T Ty s :- std.forall L (x\ std.exists x var), !, coq.error "Invalid mode for" Ty).
-
-% takes the type of a class and build a list
-% of hint mode where the last element is mandatory
-pred make-last-hint-mode-input i:term, o:list hint-mode.
-make-last-hint-mode-input (prod _ _ (x\ (prod _ _ _) as T)) [mode-output | L] :-
-  pi x\ make-last-hint-mode-input (T x) L. 
-make-last-hint-mode-input (prod _ _ _) [mode-input].
-make-last-hint-mode-input (sort _) [].
-
-% build a list of the seme langht as the the passed one
-% where all the elements are []
-pred build-empty-list i:list B, o:list (list A).
-build-empty-list [] [].
-build-empty-list [_ | TL] [[] | L] :- 
-  build-empty-list TL L.
-
-% add the hint modes of a Class to the database.
-% note that if the Class has not specified hint mode
-% then we assume the hint mode to be - - - ... !
-pred add-modes i:gref.
-:if "add-modes"
-add-modes GR :-
-  % the hint mode is added only if not exists
-  if (not (tc.class GR _ _)) (
-    coq.env.typeof GR Ty,
-    coq.hints.modes GR "typeclass_instances" ModesProv,
-    if (ModesProv = []) (Modes = [{make-last-hint-mode-input Ty}]) (Modes = ModesProv),
-    % make-modes-cl GR [] Ty Modes {build-empty-list Modes} Cl,
-    % add-tc-db _ (after "firstHook") Cl,
-  ) true.
-add-modes _.
\ No newline at end of file
diff --git a/apps/tc/elpi/att_parser.elpi b/apps/tc/elpi/att_parser.elpi
new file mode 100644
index 000000000..fb8dd2b8d
--- /dev/null
+++ b/apps/tc/elpi/att_parser.elpi
@@ -0,0 +1,119 @@
+/* license: GNU Lesser General Public License Version 2.1 or later           */
+/* ------------------------------------------------------------------------- */
+
+/*
+  This file aims to parse the attributes passed to a class. These parsed
+  attributes are stored in the tc.pending.atts predicate.
+
+  A new pending.atts rule is built with the command TC.Pending_attributes
+
+  We call atts "pending" since atts are meant to add the wanted attributes to
+  the signature of the incoming class declaration (remember that a class in coq
+  is translated as a predicate in elpi). After the creation of the predicate the
+  pending attribute rule is removed. 
+
+  NOTE: it is forbidden to have two rules for tc.pending.atts in the same
+  database
+*/
+namespace tc {
+  namespace pending {
+
+    shorten tc.pending.{atts, mode, functionality}.
+    shorten tc.{no-backtrack}.
+
+    pred default-atts o:mode, o:functionality, o:tc.search-mode.
+    default-atts (mode []) (functionality ff) (tc.no-backtrack ff).
+
+    namespace internal {
+      % returns the bool associated to an option.
+      % by default, if not specified, ff is returned
+      pred get-bool-opt i:string, o:bool.
+      get-bool-opt S B :- get-option S B, !.
+      get-bool-opt _ ff.
+
+      namespace modes {
+        /*
+          for each option returns its value. Note that no check (for now) is
+          done to verify if the value is a valid mode. moreover, if mode is `i`
+          (resp. `o`) with flag `ff`, we return its negated version, i.e. `o`
+          (resp. `o`)
+        */
+        pred get-option->modes-string i:prop, o:string. 
+        get-option->modes-string (get-option A tt) A :- !.
+        get-option->modes-string (get-option "i" ff) "o" :- !.
+        get-option->modes-string (get-option "o" ff) "i" :- !.
+        get-option->modes-string A _ :- coq.error "[tc] cannot parse" A.
+
+        pred from-att o:mode.
+        from-att (mode Modes') :-
+          get-option "mode" L,
+          std.map L get-option->modes-string Modes, !,
+          % adding 'o' to the end of modes for the proof of instance search
+          std.append Modes ["o"] Modes'.
+        % By default, if modes are not specified, we return the empty list
+        from-att (mode []).
+      }
+
+      % [give-attribute S P R] looks for the value (of type bool) of the attribute
+      %       called S, and returns the predicate P applied to this value
+      pred give-attribute i:string, i:(bool -> B), o:B.
+      give-attribute S P (P B) :- get-bool-opt S B. 
+    }
+
+    macro @functional :- "functional".
+    macro @no-backtrack :- "no_backtrack".
+    macro @mode :- "mode".
+    macro @pending-atts! :- "pending-atts".
+
+    /*
+      parses the attributes list to retrive the declared mode, functionality and
+      search-mode. This parsing operation is for attributes of new predicates.
+      If an attribute is not provided the default value will be returned.
+
+      to extend the attribute parse:
+      - add the new label in the list passed to parse-attributes
+      - add the new value as ouput of this signature
+      - changes will be needed for the implementation of pending.atts and
+        declare-class-in-elpi predicates.
+    */
+    pred att-parser-for-pred o:mode, o:functionality, o:tc.search-mode.
+    att-parser-for-pred Modes Functional NoBacktrack :-
+      coq.parse-attributes {attributes}
+        [ att @mode attlist, 
+          att @no-backtrack bool,
+          att @functional bool, 
+          att-ignore-unknown ] Opts, !,
+      Opts => (
+        internal.modes.from-att Modes,
+        internal.give-attribute @no-backtrack no-backtrack NoBacktrack,
+        internal.give-attribute @functional functionality Functional,
+        true).
+
+    % parse attributes with att-parser-for-pred and accumulate the
+    % corressponing tc.pending.atts clause in the database
+    pred att-add.
+    att-add :-
+      atts _ _ _,
+      coq.error "[TC] an already pending attribute instruction exists".
+    att-add :- att-acc {att-parser-for-pred}, !.
+
+    % accumulates a pending.atts in the database
+    pred att-acc i:mode, i:functionality, i:tc.search-mode. 
+    att-acc Modes Functional NoBacktrack :-
+      tc.add-tc-db @pending-atts! _ (atts Modes Functional NoBacktrack).
+
+    % returns and remove the pending attributes from the database
+    pred get o:mode, o:functionality, o:tc.search-mode.
+    get Modes Functional NoBacktrack :-
+      atts Modes Functional NoBacktrack, !, att-rm.
+    get Modes Functional NoBacktrack :-
+      default-atts Modes Functional NoBacktrack.
+
+    % removes the pending attributes from the database. this removal is done
+    % after a new predicate (class) has been declared
+    pred att-rm.
+    att-rm :-
+      default-atts Modes Functional NoBacktrack,
+      tc.remove-clause @pending-atts! (atts Modes Functional NoBacktrack) [].
+  }
+}
\ No newline at end of file
diff --git a/apps/tc/elpi/compiler1.elpi b/apps/tc/elpi/compiler1.elpi
index 535bf791a..17b9dcd6e 100644
--- a/apps/tc/elpi/compiler1.elpi
+++ b/apps/tc/elpi/compiler1.elpi
@@ -89,7 +89,7 @@ namespace tc {
   build-args (prod _ _ Bo) [{{0}} | TL] :- !, build-args (Bo _) TL.
   build-args _ [{{0}}].
 
-  % [remove-inst GR] remove an instance from the DB by replacing it with `dummy`
+  % [remove-inst GR] remove an instance from the DB
   pred remove-inst i:gref.
   remove-inst InstGR :- 
     tc.get-full-path InstGR ClauseName,
diff --git a/apps/tc/elpi/create_tc_predicate.elpi b/apps/tc/elpi/create_tc_predicate.elpi
index 00e51bca7..f2367af07 100644
--- a/apps/tc/elpi/create_tc_predicate.elpi
+++ b/apps/tc/elpi/create_tc_predicate.elpi
@@ -4,41 +4,30 @@
 namespace tc {
   shorten tc.{search-mode}.
 
-  % The predicate of a class is local if inside a section and readded at section end.
-  % This way, section variables are generalized
+  % The predicate of a class is local if inside a section and readded at section
+  % end. This way, section variables are generalized
   pred get-class-locality o:list prop. 
   get-class-locality [@local!] :- coq.env.current-section-path [_ | _], !.
   get-class-locality [@global!].
 
-  % [add-class-gr SearchMode ClassGR] adds the predicate for the class with its corresponing mode
-  % NOTE: the mode inside TC.declare_mode has the priority over Coq mode or #[mode=(...)] TC.Declare
-  pred add-class-gr i:search-mode, i:gref.
-  % the predicate for the class has alread been added
-  add-class-gr _ ClassGR :- tc.class ClassGR _ _ _, !. 
-  add-class-gr SearchMode ClassGR :-
+  % [declare-class-in-elpi SearchMode ClassGR] adds the elpi predicate for the
+  % given class  
+  pred declare-class-in-elpi i:gref.
+  declare-class-in-elpi ClassGR :- tc.class ClassGR _ _ _, !. % Nothing is done since the predicate already exists
+  declare-class-in-elpi ClassGR :-
     std.assert! (coq.TC.class? ClassGR) "Only gref of type classes can be added as new predicates",
-    tc.get-elpi-mode ClassGR EM SM, 
+    tc.pending.get Mode Functionality_ SearchMode,
+    tc.get-elpi-mode ClassGR Mode EM SM,
     tc.gref->pred-name ClassGR PredName,
     get-class-locality Locality, 
     Locality => (
       coq.elpi.add-predicate "tc.db" _ PredName EM,
       tc.add-tc-db _ _ (tc.class ClassGR PredName SearchMode SM)).
 
-  pred add-class-str i:search-mode, i:string.
-  add-class-str SearchMode ClassStr :-
+  pred add-class-str i:string.
+  add-class-str ClassStr :-
     coq.locate ClassStr ClassGR,
-    add-class-gr SearchMode ClassGR.
-
-  pred attr->search-mode o:search-mode. 
-  attr->search-mode tc.deterministic :- get-option "deterministic" tt, !.
-  attr->search-mode tc.classic.
-
-  pred attr->modes o:list hint-mode.
-  attr->modes CoqModes :- 
-    get-option "mode" L,
-    std.map L get-key-from-option RawModes, 
-    std.map RawModes tc.string->coq-mode CoqModes, !.
-  attr->modes [].
+    declare-class-in-elpi ClassGR.
 
   pred get-key-from-option i:prop, o:string. 
   get-key-from-option (get-option A tt) A :- !.
@@ -46,38 +35,53 @@ namespace tc {
   get-key-from-option (get-option "o" ff) "i" :- !.
   get-key-from-option A _ :- coq.error A "should be an option".
 
+
+  /* 
+    CAVEAT: TC.Declare does not trasmit implicit arguments are not transmitted to the new created
+    class in Coq.
+
+    NOTE: when we declare a class in Coq, the listener (TC.Compiler) will be
+    called in order to add the corresponding predicate in the elpi database.
+    However, this call to the listener is not aware of the attributes (Modes,
+    SearchMode, Functionality...) passed to the pragma TC.Declare. Therefore the
+    `tc.class ClassGR PredName SearchMode RawModes'` is needed and has higher
+    priority of the tc.class rule added by the subsequent call to
+    `declare-class-in-coq`
+  */
   pred declare-class-in-coq i:gref.
   declare-class-in-coq ClassGR :- 
-    attr->modes CoqModes,
-    if (CoqModes = [])
+    % TODO: Functional should be taken into account
+    tc.pending.att-parser-for-pred (tc.pending.mode RawModes) _Functional SearchMode,
+
+    if (RawModes = [])
       (
-        tc.modes-of-class ClassGR EM,
-        std.map EM tc.elpi->string-mode SM
+        % now modes declared with Pending_attributes command, take the one
+        % declared in Coq
+        tc.modes-of-class ClassGR RawModes'
       )(
-        coq.hints.add-mode ClassGR "typeclass_instances" CoqModes,
-        std.map CoqModes (x\y\tc.string->coq-mode y x) SM',
-        std.append SM' ["o"] SM
+        % The next row is a conversion from string list to hint-mode list
+        std.map RawModes tc.string->coq-mode CoqModes,
+        % the last is the output carrying the instance of the rule
+        % this information must not be transmitted to coq mode signature
+        std.drop-last 1 CoqModes CoqModes',
+        coq.hints.add-mode ClassGR "typeclass_instances" CoqModes',
+        RawModes = RawModes'
       ),
-    % CAVEAT: this triggers the observer
+    
+    % this triggers the observer TC.Compiler
     coq.TC.declare-class ClassGR,
-    attr->search-mode SearchMode, 
     tc.gref->pred-name ClassGR PredName,
-    % HACK: we override the clauses added by the observer, since it does not know
-    % the SearchMode.
     get-class-locality Locality, 
-    
-    Locality => tc.add-tc-db _ (after "0") (tc.class ClassGR PredName SearchMode SM :- !).
+    Locality => tc.add-tc-db _ (after "0") (tc.class ClassGR PredName SearchMode RawModes' :- !).
 
   pred declare-class i:indt-decl. 
   declare-class D :- !, 
     coq.env.add-indt D I,
-    coq.parse-attributes {attributes} 
-      [ att "mode" attlist, att "deterministic" bool ] Opts,
-    Opts => declare-class-in-coq (indt I).
+    declare-class-in-coq (indt I).
 
-  % Contains some instruction that are executed just after the creation of
-  % the predicate for the class
-  namespace eta-reduction-aux {
+  % Contains some instruction that are executed just after the creation of the
+  % predicate for the class
+  namespace dead-code-eta-reduction-aux {
     pred is-functional i:term.
     is-functional (prod _ _ _).
 
diff --git a/apps/tc/elpi/ho_compile.elpi b/apps/tc/elpi/ho_compile.elpi
index 498883ed1..835682f8f 100644
--- a/apps/tc/elpi/ho_compile.elpi
+++ b/apps/tc/elpi/ho_compile.elpi
@@ -1,3 +1,6 @@
+/* license: GNU Lesser General Public License Version 2.1 or later           */
+/* ------------------------------------------------------------------------- */
+
 namespace tc {
   shorten tc.{r-ar, range-arity}.
 
@@ -217,8 +220,8 @@ namespace tc {
         (pi a b c\ tc.get-TC-of-inst-type (tc.prod-range a c) b :- tc.get-TC-of-inst-type a b) => 
           tc.get-TC-of-inst-type PTy TC, !,
         compile-ty L L1 P {neg IsPositive} PTy [] [] NewPrem,
-        if (tc.class TC _ tc.deterministic _)
-          (NewPrem' = do-once NewPrem)
+        if (tc.class TC _ (tc.no-backtrack tt) _)
+          (NewPrem' = std.once NewPrem)
           (NewPrem' = NewPrem),
         compile-ty L1 L2 ProofHd IsPositive ITy ProofTlR [NewPrem' | PremR] Clause.
       compile-premise L L1 _ _ ProofHd IsPositive ITy ProofTlR PremR Clause :-
diff --git a/apps/tc/elpi/ho_precompile.elpi b/apps/tc/elpi/ho_precompile.elpi
index dd5bf3a28..6bae78904 100644
--- a/apps/tc/elpi/ho_precompile.elpi
+++ b/apps/tc/elpi/ho_precompile.elpi
@@ -107,7 +107,6 @@ namespace tc {
       precompile-aux _ (sort _ as C) A C A :- !.
 
       % Detect maybe-eta term
-      % TODO: should I precompile also the type of the fun and put it in the output term
       precompile-aux _ (fun Name Ty B as T) N (tc.maybe-eta-tm (fun Name Ty B') Scope) (s M) :-
         maybe-eta T, !,
         free-var Scope,
@@ -185,7 +184,6 @@ namespace tc {
       :index (_ _ 1)
       pred may-contract-to i:list term, i:term, i:term.
       may-contract-to _ N N :- !.
-      % TODO: here we should do var V _ Scope and use scope: N can be in Scope but not in S
       may-contract-to L N (app [V|S]) :- var V, !,
         std.forall [N|L] (x\ exists! S (may-contract-to [] x)).
       may-contract-to L N (app [N|A]) :-
@@ -202,7 +200,6 @@ namespace tc {
       occurs-rigidly N (fun _ _ B) :- pi x\ occurs-rigidly N (B x).
 
       pred maybe-eta-aux i:term, i:list term.
-      % TODO: here we should do var V _ Scope and use Scope: an elt in L can appear in Scope
       maybe-eta-aux (app[V|S]) L :- var V, !,
         std.forall L (x\ exists! S (y\ may-contract-to [] x y)).
       maybe-eta-aux (app [_|A]) L :-
diff --git a/apps/tc/elpi/modes.elpi b/apps/tc/elpi/modes.elpi
index d3e72aaec..a07514551 100644
--- a/apps/tc/elpi/modes.elpi
+++ b/apps/tc/elpi/modes.elpi
@@ -1,3 +1,6 @@
+/* license: GNU Lesser General Public License Version 2.1 or later           */
+/* ------------------------------------------------------------------------- */
+
 namespace tc {
   shorten tc.{pending-mode}.
 
@@ -6,56 +9,75 @@ namespace tc {
   typeabbrev string-modeL (list string).
   macro @pending-mode! :- "pending mode".
 
-  pred string->coq-mode o:string, o:hint-mode.
-  string->coq-mode uvar uvar :- coq.error "[TC] string->coq-mode". 
-  string->coq-mode "!" mode-input :- !.
-  string->coq-mode "+" mode-ground :- !.
-  string->coq-mode "-" mode-output :- !.
-  string->coq-mode "bang" mode-ground :- !.
-  string->coq-mode "plus" mode-input :- !.
-  string->coq-mode "minus" mode-output :- !.
-  string->coq-mode "i" mode-input :- !.
-  string->coq-mode "o" mode-output :- !.
-  string->coq-mode A _ :- coq.error A "is not a valid mode".
-
-  pred coq->elpi-mode i:hint-mode, o:elpi-mode.
-  :name "coq->elpi-mode"
-  coq->elpi-mode mode-ground (pr in "term"). % approximation
-  /*
-    The coq input-mode corresponds to the elpi mode out
-    Instance : option_equiv : ∀ {A : Type}, Equiv A → Equiv (option A)
-    Mode:      Equiv !
-    Check _ :  forall x, Equiv A -> Equiv (option _). 
-    In coq, the Check gives the instance option_equiv
-    In elpi, we would have the rule: `tc-Equiv (option A) (option_equiv A B) :- tc-equiv A B.`
-            since the argument in first position of the premise is flexible, then we have a failure
-  */
-  coq->elpi-mode mode-input (pr out "term").
-  coq->elpi-mode mode-output (pr out "term").
+  pred is-mode-ground i:string.
+  is-mode-ground "plus".
+  is-mode-ground "ground".
+  is-mode-ground "g".
+  is-mode-ground "+".
+
+  pred is-mode-ouput i:string.
+  is-mode-ouput "o".
+  is-mode-ouput "-".
+  is-mode-ouput "minus".
+
+  pred is-mode-input i:string.
+  is-mode-input "bang".
+  is-mode-input "i".
+  is-mode-input "!".
+
+  pred string->coq-mode i:string, o:hint-mode.
+  string->coq-mode S mode-ground :- is-mode-ground S, !.
+  string->coq-mode S mode-output :- is-mode-ouput S, !.
+  string->coq-mode S mode-input  :- is-mode-input S, !.
+  string->coq-mode A B :- coq.error "[TC] string->coq-mode:" A "," B "is not a valid mode".
 
   pred string->elpi-mode i:string, o:elpi-mode.
-  string->elpi-mode S R :- coq->elpi-mode {string->coq-mode S} R, !.
-  string->elpi-mode _ (pr out "term").
+  string->elpi-mode uvar uvar :- coq.error "[TC] string->elpi-mode call with 2 flex args".
+
+  /*  
+    this is an approximation!
+    the input mode of coq tests that the arg has a rigid head.
+    e.g. (tc-Eq (list nat) => tc-Eq (list X))
+    in coq succeeds, in elpi it does not...
+    to solve the issue we cast coq-input in elpi-output :-)
+  */
+  string->elpi-mode S (pr out "term")  :- is-mode-input S, !.
 
-  pred elpi->string-mode i:elpi-mode, o:string.
-  elpi->string-mode (pr in _) "i" :- !.
-  elpi->string-mode (pr out _) "o".
+  /* 
+    here another approximation!
+    the ground-mode of coq tests that the args is ground.
+    e.g (tc-CatchAll X => tc-CatchAll (list X))
+    succeeds in elpi but not in coq...
+  */
+  string->elpi-mode S (pr in "term")  :- is-mode-ground S, !.
+
+  /*
+    output is the only compatible mode!
+  */
+  string->elpi-mode S (pr out "term") :- is-mode-ouput S, !.
+  string->elpi-mode A B :- coq.error "[TC] the call `string->elpi-mode" A B "` is not valid".
+
+  pred coq->string-mode i:hint-mode, o:string.
+  coq->string-mode mode-ground "g".
+  coq->string-mode mode-input "i".
+  coq->string-mode mode-output "o".
 
   % 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 (elpi-mode).
+  pred modes-of-class i:gref, o:list string.
   modes-of-class ClassGR Modes :- 
     coq.hints.modes ClassGR "typeclass_instances" CoqModesList,
-    not (CoqModesList = []),
-    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} ")"),
+    if (CoqModesList = [_,_|_])
+      (coq.warning "TC.Modes" "an elpi predicate has one mode, the class" {coq.gref->string ClassGR} "has" {std.length CoqModesList} "(all arguments will be put in output mode)", fail)
+      true,
     CoqModesList = [HintModesFst],
-    std.append {std.map HintModesFst coq->elpi-mode} [pr out "term"] Modes.
+    std.append {std.map HintModesFst coq->string-mode} ["o"] Modes.
   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.
+    list-init N (x\r\ r = "o") Modes.
 
   pred add-pending-mode i:list string.
   add-pending-mode _ :-
@@ -75,15 +97,15 @@ namespace tc {
     N' is N + 1,
     std.assert! (std.length L N') "Pending mode invalid for class GR".
 
-  pred get-elpi-mode i:gref, o:elpi-modeL, o:string-modeL.
-  get-elpi-mode ClassGR EM SM :-
-    pending-mode SM, !,
+  pred get-elpi-mode i:gref, i:tc.pending.mode, o:elpi-modeL, o:string-modeL.
+  % empty pending mode list, means that we look for modes declared in coq
+  get-elpi-mode ClassGR (tc.pending.mode []) EM SM :- !,
+    modes-of-class ClassGR SM, 
+    std.map SM string->elpi-mode EM.
+  % we have 
+  get-elpi-mode ClassGR (tc.pending.mode SM) EM SM :-
     check-pending-mode-arity ClassGR SM, 
-    remove-pending-mode,
     std.map SM string->elpi-mode EM.
-  get-elpi-mode ClassGR EM SM :-
-    modes-of-class ClassGR EM, 
-    std.map EM elpi->string-mode SM.
 
   pred get-evars i:term, o:list term.
   get-evars T L :-
@@ -96,14 +118,24 @@ namespace tc {
   action-to-accumulate _ T [evars HD] :- var T HD _, !.
   action-to-accumulate _ _ [].
 
-  pred mode-check i:string, i:term.
-  % heuristic: if we are in "+" mode, then all evars in T should only be 
-  %            in that argument
-  mode-check "+" T :- !, 
+  pred mode-check-ground i:term.
+  % heuristic: all evars in T should only be in that argument
+  mode-check-ground T :-
     std.findall-unary evars L,
     get-evars T EV,
     std.forall EV (x\ std.forall L (x'\ not (x == x'))).
-  mode-check "!" uvar :- !, fail.
+
+  pred mode-check i:string, i:term.
+  % approximation only at top level we check that the argument in ground mode
+  % (for Coq) is groud. During the recursive calls, since we use elpi input
+  % mode, we don't verify this property anymore
+  mode-check S T :- is-mode-ground S, !, mode-check-ground T.
+
+  % approximation: only at top level we check that the argument in input mode
+  % (for Coq) is not flex (i.e. has a rigid head). During the recursive calls,
+  % since we use elpi output mode (see rules for string->elpi-mode) we stop
+  % verifying this property
+  mode-check S uvar :- is-mode-input S, !, fail.
   mode-check _ _.
 
   pred modes-check.aux i:list string, i:list term.
@@ -116,6 +148,8 @@ namespace tc {
       P => modes-check.aux XS YS            % accumulate P and iterate of XS YS 
     ].
 
+  % used by the solver to check that the top level arguments respects the modes
+  % declared in coq
   pred modes-check i:term.
   modes-check (global _).
   modes-check (pglobal _ _).
@@ -124,4 +158,8 @@ namespace tc {
     tc.get-mode ClassGR M,
     std.drop-last 1 M M',
     modes-check.aux M' Args.
+
+  pred get-mode i:gref, o:list string.
+  get-mode ClassGR M :- tc.class ClassGR _ _ M, !.
+  get-mode ClassGR _ :- coq.error "[TC]" ClassGR "is an unknown class".
 }
diff --git a/apps/tc/elpi/tc_aux.elpi b/apps/tc/elpi/tc_aux.elpi
index 4946bd033..2e8f86d99 100644
--- a/apps/tc/elpi/tc_aux.elpi
+++ b/apps/tc/elpi/tc_aux.elpi
@@ -33,11 +33,6 @@ namespace tc {
     coq.safe-dest-app T HD _,
     not (var HD), class-gref HD ClassGR.
 
-  pred drop-last i:list A, i:list A, o:list A.
-  drop-last [X | XS] [Y | YS] L :-
-    same_term X Y, !, drop-last XS YS L.
-  drop-last L [] L' :- std.rev L L'.
-
   pred instances-of-current-section o:list gref.
   :name "MySectionEndHook"
   instances-of-current-section InstsFiltered :-
@@ -79,14 +74,6 @@ namespace tc {
     get-TC-of-inst-type T Hd, 
     coq.TC.class? Hd. 
 
-  % input (∀ a, b, c ... => app [A, B, ..., Last])
-  % returns Last 
-  pred get-last i:term, o:term.
-  get-last (prod _ _ Bo) R :-
-    pi x\ get-last (Bo x) R.
-  get-last (app L) R :-
-    std.last 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 :-
@@ -101,16 +88,6 @@ namespace tc {
     rex.replace "ö" "o" {coq.gref->id Gr} GrStr,
     S is "tc-" ^ Path ^ GrStr.
 
-  pred no-backtrack i:list prop, o:list prop. 
-  no-backtrack [] [].
-  no-backtrack [do X | XS] [std.do! [(std.do! X') | XS']] :- !, 
-    no-backtrack X X', no-backtrack XS XS'.
-  no-backtrack [X | XS] [std.do! [X | XS']] :- !, no-backtrack XS XS'.
-
-  pred get-mode i:gref, o:list string.
-  get-mode ClassGR M :- tc.class ClassGR _ _ M, !.
-  get-mode ClassGR _ :- coq.error "[TC]" ClassGR "is an unknown class".
-
   /* 
   [make-tc.aux B Sol Head Body Rule] builds the rule with the given Head and body
                                     paying attention to the positivity of the
@@ -127,9 +104,20 @@ namespace tc {
   make-tc.aux tt _ Head Body (Head :- Body) :- !.
   make-tc.aux ff Sol Head Body P :- !, P = if (var Sol) (Body => Head) true.
 
+  /*
+    [make-tc InstTy Sol RuleBody IsPositive Rule]
+    - InstTy is the type of a class where all prod have been eaten by the
+      compiling phase. If some of these prod are type-classes then they are
+      collected in `RuleBody`
+    - Sol is the name of the instance being compiled
+    - IsPositive tell if the we are in positive or negative position.
+    - Rule is the rule to add in the database of instance, i.e. the compiled
+      instance. Note that `Rule` is not a closed term, it contains quantified
+      variables but no `pi` in front of it. It is the compiler which accumulates
+  */
   pred make-tc i:term, i:term, i:list prop, i:bool, o:prop.
-  make-tc Goal Sol RuleBody IsPositive Rule :-
-    coq.safe-dest-app Goal Class Args,
+  make-tc InstTy Sol RuleBody IsPositive Rule :-
+    coq.safe-dest-app InstTy Class Args,
     get-TC-of-inst-type Class ClassGR,
     gref->pred-name ClassGR ClassStr,
     std.append Args [Sol] ArgsSol, 
@@ -165,8 +153,6 @@ namespace tc {
     coq.redflags.add coq.redflags.nored [coq.redflags.beta, coq.redflags.delta | UnfoldRF] RF,
     @redflags! RF => coq.reduction.lazy.norm G1 G2.
 
-  pred dummy.
-
   pred remove-clause i:string, i:prop, i:list prop.
   remove-clause ClauseName P Locality :-
     %Locality => add-tc-db _ (remove ClauseName) P.
diff --git a/apps/tc/examples/tutorial.v b/apps/tc/examples/tutorial.v
index fa780cb10..c9e7d360e 100644
--- a/apps/tc/examples/tutorial.v
+++ b/apps/tc/examples/tutorial.v
@@ -77,9 +77,9 @@ TC.Print_instances Eqb.
 TC.Get_class_info Eqb.
 
 Module Backtrack.
-  Elpi TC Solver Override TC.Solver All.
+
+  #[no_backtrack] TC.Pending_attributes.
   Class NoBacktrack (n: nat).
-  TC.Set_deterministic NoBacktrack.
   Class A (n: nat).
 
   Instance a0 : A 0. Qed.
diff --git a/apps/tc/tests/nobacktrack.v b/apps/tc/tests/nobacktrack.v
index b95f7f5d6..2079eaef3 100644
--- a/apps/tc/tests/nobacktrack.v
+++ b/apps/tc/tests/nobacktrack.v
@@ -5,8 +5,8 @@ Set TC NameShortPath.
 
 Module A.
 
+  #[no_backtrack] TC.Pending_attributes.
   Class C (n : nat) := {}.
-  Elpi TC.Set_deterministic C.
   Elpi TC.Get_class_info C.
   Local Instance c_1 : C 1 | 10 := {}.
   Local Instance c_2 : C 2 | 1 := {}.
@@ -28,8 +28,8 @@ End A.
 
 Module B.
 
+  #[no_backtrack] TC.Pending_attributes.
   Class A (T : Set) := f : T -> T.
-  Elpi TC.Set_deterministic A.
 
   Global Instance A1 : A bool := {f x := x}.
   Global Instance A2 `(A bool) : A (bool * bool) := 
diff --git a/apps/tc/tests/section_in_out.v b/apps/tc/tests/section_in_out.v
index 8360892db..2f3aa7865 100644
--- a/apps/tc/tests/section_in_out.v
+++ b/apps/tc/tests/section_in_out.v
@@ -17,11 +17,13 @@ Elpi Accumulate lp:{{
     WantedLength is {origial_tc} + Len,
     std.assert! ({std.length R} = WantedLength) 
       "Unexpected number of instances",
-    std.forall R (x\ sigma L\
-      std.assert! (count R x L, L = 1) "Duplicates in instances"). 
+    std.forall R (x\ sigma L\ count R x L,
+      if (L = 1) true
+        (coq.error "Duplicate instances for class" x ": expected 1, found" L)). 
 }}.
 
 Elpi Query TC.Solver lp:{{
+  sigma Rules Len\
   std.findall (tc.instance _ _ _ _) Rules,
   std.length Rules Len,
   coq.elpi.accumulate _ "tc.db" (clause _ _ (origial_tc Len)).
diff --git a/apps/tc/tests/test_pending_mode.v b/apps/tc/tests/test_pending_mode.v
index 9639a611a..6a303d393 100644
--- a/apps/tc/tests/test_pending_mode.v
+++ b/apps/tc/tests/test_pending_mode.v
@@ -2,7 +2,7 @@ From elpi Require Import tc.
 Require Import Bool.
 
 Module m1.
-  Elpi TC.Pending_mode +.
+  #[mode(g)] Elpi TC.Pending_attributes.
   Class C (i : nat).
   Instance C0 : C 0. Qed.
   Goal exists x, C x. eexists. Fail apply _. Abort.
@@ -10,8 +10,8 @@ Module m1.
   Instance C0' : C' 0. Qed.
   Goal exists x, C' x. eexists. apply _. Abort.
 
-  Elpi TC.Pending_mode +.
-  Fail Elpi TC.Pending_mode +.
+  #[mode(g)] TC.Pending_attributes.
+  Fail #[mode(g)] TC.Pending_attributes.
 
   Class C'' (i : nat).
   Instance C0'' : C'' 0. Qed.
@@ -19,7 +19,7 @@ Module m1.
 End m1.
 
 Module ground.
-  Elpi TC.Pending_mode +.
+  #[mode(g)] TC.Pending_attributes.
   Class C (i : Type).
   Instance i : C (list nat). Qed.
 
@@ -30,7 +30,7 @@ Module ground.
 End ground.
 
 Module ground1.
-  Elpi TC.Pending_mode +.
+  #[mode(g)] TC.Pending_attributes.
   Class C (i : Type).
   Instance i x: C x. Qed.
 
@@ -41,7 +41,7 @@ Module ground1.
 End ground1.
 
 Module ground2.
-  Elpi TC.Pending_mode +.
+  #[mode(g)] TC.Pending_attributes.
   Class C (i : Type).
   Instance i (x: Type): C (list x). Qed.
 
@@ -52,7 +52,7 @@ Module ground2.
 End ground2.
 
 Module ground3.
-  Elpi TC.Pending_mode + +.
+  #[mode(g,g)] TC.Pending_attributes.
   Class C {i : Type} (f : i -> i -> Prop).
   Instance i {X : Type}: C (@eq X). Qed.
   Hint Mode C ! ! : typeclass_instances.
@@ -64,10 +64,9 @@ Module ground3.
 End ground3.
 
 Module ground4.
-  Elpi TC.Pending_mode - +.
+  #[mode(o,g)] TC.Pending_attributes.
   Class C {i : Type} (f : i -> i -> Prop).
   Instance i {X : Type}: C (@eq X). Qed.
-  Hint Mode C ! ! : typeclass_instances.
 
   Goal exists (X : Type), @C (list X) eq. 
     eexists.
@@ -76,10 +75,9 @@ Module ground4.
 End ground4.
 
 Module rigid_head1.
-  Elpi TC.Pending_mode !.
+  #[mode(i)] TC.Pending_attributes.
   Class C (i : Type).
   Instance i: C (list nat). Qed.
-  Hint Mode C ! : typeclass_instances.
 
   Goal exists (x : Type), C (list x). 
     eexists.
@@ -88,15 +86,15 @@ Module rigid_head1.
 
   Goal exists (x : Type), C x. 
     eexists.
+    (* This fails since x is flex and mode i accepts only terms with rigid head *)
     Fail apply _.
   Abort.
 End rigid_head1.
 
 Module rigid_head2.
-  Elpi TC.Pending_mode ! !.
+  #[mode(i,i)] TC.Pending_attributes.
   Class C {i : Type} (f : i -> i -> Prop).
   Instance i {X : Type}: C (@eq X). Qed.
-  Hint Mode C ! ! : typeclass_instances.
 
   Goal exists (X : Type), C (@eq X). 
     eexists.
@@ -106,7 +104,7 @@ End rigid_head2.
 
 Module simplEq.
 
-  TC.Pending_mode "!".
+  #[mode(i)] TC.Pending_attributes.
   Class MyEqb A : Type := eqb : A -> A -> bool.
   (* Global Hint Mode MyEqb ! : typeclass_instances. *)
 
@@ -122,7 +120,7 @@ Module simplEq.
 End simplEq.
 
 Module force_input_link.
-  TC.Pending_mode "+".
+  #[mode(g)] TC.Pending_attributes.
   Class A (i: nat -> nat -> nat).
 
   Global Hint Mode A + : typeclass_instances.
@@ -140,7 +138,7 @@ End force_input_link.
 
 Module force_input_link_HO_var1.
 
-  TC.Pending_mode !.
+  #[mode(i)] TC.Pending_attributes.
   Class A (i: Type).
   Global Hint Mode A ! : typeclass_instances. (*Mode also added in elpi*)
 
@@ -163,7 +161,7 @@ End force_input_link_HO_var1.
 
 Module force_input_link_HO_var2.
 
-  TC.Pending_mode !.
+  #[mode(i)] TC.Pending_attributes.
   Class A (i: Type).
   Global Hint Mode A ! : typeclass_instances. (*Mode also added in elpi*)
 
@@ -184,7 +182,7 @@ End force_input_link_HO_var2.
 
 Module force_input_link_HO_var3.
 
-  TC.Pending_mode !.
+  #[mode(i)] TC.Pending_attributes.
   Class A (i: Type).
   Global Hint Mode A ! : typeclass_instances. (*Mode also added in elpi*)
 
diff --git a/apps/tc/tests/test_tc_declare.v b/apps/tc/tests/test_tc_declare.v
index 1c51a9f09..f18672926 100644
--- a/apps/tc/tests/test_tc_declare.v
+++ b/apps/tc/tests/test_tc_declare.v
@@ -17,7 +17,7 @@ End S1.
 (* Deterministic class test *)
 Section S2.
 
-  #[deterministic] TC.Declare Class class2 (n : nat).
+  #[no_backtrack] TC.Declare Class class2 (n : nat).
 
   Instance inst2  : class2 1 | 0. Proof. apply Build_class2. Qed.
   Instance inst2' : class2 2 | 1. Proof. apply Build_class2. Qed.
diff --git a/apps/tc/theories/add_commands.v b/apps/tc/theories/add_commands.v
index fcecf6d33..738d60bb4 100644
--- a/apps/tc/theories/add_commands.v
+++ b/apps/tc/theories/add_commands.v
@@ -14,30 +14,21 @@ From elpi.apps.tc.elpi Extra Dependency "ho_link.elpi" as ho_link.
 From elpi.apps.tc.elpi Extra Dependency "parser_addInstances.elpi" as parser_addInstances.
 From elpi.apps.tc.elpi Extra Dependency "solver.elpi" as solver.
 From elpi.apps.tc.elpi Extra Dependency "create_tc_predicate.elpi" as create_tc_predicate.
+From elpi.apps.tc.elpi Extra Dependency "att_parser.elpi" as att_parser.
 
 Set Warnings "+elpi".
 
 Elpi Command TC.AddAllInstances.
 Elpi Accumulate Db tc.db.
-Elpi Typecheck.
 Elpi Accumulate Db tc_options.db.
-Elpi Typecheck.
 Elpi Accumulate File base.
-Elpi Typecheck.
 Elpi Accumulate File tc_aux.
-Elpi Typecheck.
 Elpi Accumulate File ho_precompile.
-Elpi Typecheck.
 Elpi Accumulate File unif.
-Elpi Typecheck.
 Elpi Accumulate File ho_link.
-Elpi Typecheck.
 Elpi Accumulate File ho_compile.
-Elpi Typecheck.
 Elpi Accumulate File compiler1.
-Elpi Typecheck.
 Elpi Accumulate File modes.
-Elpi Typecheck.
 Elpi Accumulate lp:{{  
   main L :- 
     args->str-list L L1,
@@ -69,12 +60,13 @@ Elpi Accumulate Db tc_options.db.
 Elpi Accumulate File base.
 Elpi Accumulate File tc_aux.
 Elpi Accumulate File modes.
+Elpi Accumulate File att_parser.
 Elpi Accumulate File create_tc_predicate.
 Elpi Accumulate lp:{{
   % 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,
-    tc.time-it _ (std.forall {coq.TC.db-tc} (x\ if (std.mem IgnoreGR x) true (tc.add-class-gr tc.classic x))) "TC.AddAllClasses".
+    tc.time-it _ (std.forall {coq.TC.db-tc} (x\ if (std.mem IgnoreGR x) true (tc.declare-class-in-elpi x))) "TC.AddAllClasses".
 }}.
 Elpi Typecheck.
 
@@ -84,17 +76,10 @@ Elpi Accumulate Db tc_options.db.
 Elpi Accumulate File base.
 Elpi Accumulate File tc_aux.
 Elpi Accumulate File modes.
+Elpi Accumulate File att_parser.
 Elpi Accumulate File create_tc_predicate.
 Elpi Accumulate lp:{{
-  pred tc.add-all-classes i:list argument , i:tc.search-mode.
-  tc.add-all-classes L S :-
-    tc.time-it _ (std.forall {args->str-list L} (tc.add-class-str S)) "TC.AddClasses".
-
-  main L :-
-    std.mem {attributes} (attribute "deterministic" _),
-    tc.add-all-classes L tc.deterministic.
-  main L :- tc.add-all-classes L tc.classic.
-  main _ :- coq.error "This commands accepts: [classic|deterministic]? TC-names*".
+  main L :- tc.time-it _ (std.forall {args->str-list L} (tc.add-class-str)) "TC.AddClasses".
 }}.
 Elpi Typecheck.
 
@@ -135,36 +120,33 @@ Elpi Accumulate Db tc_options.db.
 Elpi Accumulate File base.
 Elpi Accumulate File tc_aux.
 Elpi Accumulate File modes.
+Elpi Accumulate File att_parser.
 Elpi Accumulate File create_tc_predicate.
 Elpi Accumulate lp:{{
-  main _ :- coq.warning "TC.Declare" {tc.warning-name} 
-"This command does not fully mirror the watned behavior if the class has methods
-with implicit arguments (those implicits will be neglected)", fail.
+%   main _ :- coq.warning "TC.Declare" {tc.warning-name} 
+% "This command does not fully mirror the watned behavior if the class has methods
+% with implicit arguments (those implicits will be neglected)", fail.
   main [indt-decl D] :- tc.declare-class D.
   main _ :- coq.error "Argument should be an inductive type".
 }}.
 Elpi Typecheck.
 
-Elpi Command TC.Pending_mode.
+Elpi Command TC.Pending_attributes.
 Elpi Accumulate Db tc.db.
 Elpi Accumulate Db tc_options.db.
 Elpi Accumulate File base.
 Elpi Accumulate File tc_aux.
 Elpi Accumulate File modes.
-Elpi Accumulate File create_tc_predicate.
-Elpi Accumulate lp:{{
-  main M :- 
-    % the "o" added at the end of M stands for the solution of the goal 
-    std.append M [str "o"] M1,
-    tc.add-pending-mode {args->str-list M1}.
+Elpi Accumulate File att_parser.
+Elpi Accumulate TC.Pending_attributes lp:{{
+  main [] :- tc.pending.att-add.
 }}.
 Elpi Typecheck.
 
-
 Elpi Export TC.AddAllClasses.
 Elpi Export TC.AddAllInstances.
 Elpi Export TC.AddClasses.
 Elpi Export TC.AddInstances.
 Elpi Export TC.AddHook.
 Elpi Export TC.Declare.
-Elpi Export TC.Pending_mode.
\ No newline at end of file
+Elpi Export TC.Pending_attributes.
\ No newline at end of file
diff --git a/apps/tc/theories/db.v b/apps/tc/theories/db.v
index 45d152d99..697e33852 100644
--- a/apps/tc/theories/db.v
+++ b/apps/tc/theories/db.v
@@ -70,8 +70,7 @@ Elpi Db tc.db lp:{{
     % deterministic :- no backtrack after having found a solution/fail
     % classic       :- the classic search, if a path is failing, we backtrack
     kind search-mode type.
-    type deterministic  search-mode.
-    type classic        search-mode.
+    type no-backtrack   bool -> search-mode.
 
     % [instance Path InstGR ClassGR Locality], ClassGR is the class implemented by InstGR
     % Locality is either the empty list, or [@local!], or [@global!]
@@ -96,8 +95,16 @@ Elpi Db tc.db lp:{{
 
     pred pending-mode o:list string.
 
-    pred dummy.
-
     pred ho-link o:term, i:term, o:A.
+
+    namespace pending {
+      kind mode type.
+      type mode list string -> mode.
+
+      kind functionality type.
+      type functionality bool -> functionality.
+
+      pred atts o:mode, o:functionality, o:search-mode.
+    }
   }
 }}.
diff --git a/apps/tc/theories/tc.v b/apps/tc/theories/tc.v
index fb02013c5..7fb6cd041 100644
--- a/apps/tc/theories/tc.v
+++ b/apps/tc/theories/tc.v
@@ -14,6 +14,7 @@ From elpi.apps.tc.elpi Extra Dependency "unif.elpi" as unif.
 From elpi.apps.tc.elpi Extra Dependency "ho_link.elpi" as ho_link.
 From elpi.apps.tc.elpi Extra Dependency "solver.elpi" as solver.
 From elpi.apps.tc.elpi Extra Dependency "create_tc_predicate.elpi" as create_tc_predicate.
+From elpi.apps.tc.elpi Extra Dependency "att_parser.elpi" as att_parser.
 
 From elpi.apps Require Import db.
 From elpi.apps Require Export add_commands.
@@ -59,6 +60,7 @@ Elpi Accumulate File compiler1.
 Elpi Accumulate File create_tc_predicate.
 Elpi Accumulate File modes.
 Elpi Accumulate File solver.
+Elpi Accumulate File att_parser.
 Elpi Query lp:{{
   sigma Options\ 
     tc.all-options Options,
@@ -89,6 +91,7 @@ Elpi Accumulate File unif.
 Elpi Accumulate File ho_link.
 Elpi Accumulate File compiler1.
 Elpi Accumulate File modes.
+Elpi Accumulate File att_parser.
 Elpi Accumulate lp:{{
 
   /* 
@@ -103,8 +106,9 @@ Elpi Accumulate lp:{{
     This problem is due to the order in which the registers for Instance and
     Class creation are run.
     The solution is to do the following two jobs when a class C is created:
-      1: for every projection P of C, if P is a coercion, the wrongly 
-        compiled instance is replaced with a `dummy` clause.
+      1: for every projection P of C, if P is a coercion, P is wrongly
+        compiled since it doesn't have C as hypothesis. Therefore P is 
+        removed from the elpi db.
       2: the predicate for the class is created
       3: for every projection P of C, if P is a coercion, the correct
         instance is created and added to the db
@@ -121,34 +125,18 @@ Elpi Accumulate lp:{{
 
   main [str "new_class", str Cl] :- !,
     tc.time-it tc.oTC-time-compile-class (
-      coq.locate Cl GR, tc.add-class-gr tc.classic GR
+      coq.locate Cl GR, tc.declare-class-in-elpi GR
     ) "Compiler for Class".
 
   % used to build ad-hoc instance for eta-reduction on the argument of 
   % Cl that have function type
-  main [str "default_instance", str Cl] :- !,
-    tc.eta-reduction-aux.main Cl.
+  % main [str "default_instance", str Cl] :- !,
+  %   tc.eta-reduction-aux.main Cl.
 
   main A :- coq.error "Fail in TC.Compiler: not a valid input entry" A.
 }}.
 Elpi Typecheck.
 
-(* Command allowing to set if a TC is deterministic. *)
-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] :- 
-    coq.locate ClassStr ClassGR, 
-    std.assert! (coq.TC.class? ClassGR) "Should pass the name of a type class",
-    std.assert! (tc.class ClassGR PredName _ Modes) "Cannot find `class ClassGR _ _` in the db",
-    std.assert! (not (tc.instance _ _ ClassGR _)) "Cannot set deterministic a class with an already existing instance",
-    tc.add-tc-db _ (after "0") (tc.class ClassGR PredName tc.deterministic Modes :- !).
-}}.
-Elpi Typecheck.
-
 Elpi Command TC.Get_class_info.
 Elpi Accumulate Db tc.db.
 Elpi Accumulate Db tc_options.db.
@@ -199,7 +187,6 @@ Elpi Export TC.Print_instances.
 Elpi Export TC.Solver.
 Elpi Export TC.Compiler.
 Elpi Export TC.Get_class_info.
-Elpi Export TC.Set_deterministic.
 Elpi Export TC.Unfold.
 
 Set Warnings "elpi".
diff --git a/src/coq_elpi_builtins.ml b/src/coq_elpi_builtins.ml
index 8e3dc692f..073e4b665 100644
--- a/src/coq_elpi_builtins.ml
+++ b/src/coq_elpi_builtins.ml
@@ -468,7 +468,7 @@ let get_instance_prio gr env sigma (hint_priority : int option) : tc_priority =
          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 get_instance_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
@@ -515,7 +515,7 @@ let get_instances (env: Environ.env) (sigma: Evd.evar_map) tc : type_class_insta
     | Constr.Const (a, _) -> Some (Names.GlobRef.ConstRef a)
     | Constr.Construct (a, _) -> Some (Names.GlobRef.ConstructRef a)
     | _ -> None) constrs in
-  let isnt_of_tc = get_isntances_of_tc env sigma tc in
+  let isnt_of_tc = get_instance_of_tc env sigma tc in
   List.map (get_instance env sigma isnt_of_tc) instances_grefs
 
 let set_accumulate_to_db_interp, get_accumulate_to_db_interp =
@@ -2821,7 +2821,7 @@ Supported attributes:
     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 inst_of_tc = get_instance_of_tc env sigma class_gr in
       let {priority} = get_instance env sigma inst_of_tc inst_gr in 
       !: priority)),
   DocAbove);