diff --git a/apps/tc/elpi/compile_goal.elpi b/apps/tc/elpi/compile_goal.elpi
index 5e9e8bf94..340c76f60 100644
--- a/apps/tc/elpi/compile_goal.elpi
+++ b/apps/tc/elpi/compile_goal.elpi
@@ -35,11 +35,6 @@ namespace tc {
       pred maybe-eta i:term.
       maybe-eta (fun _ _ B) :- pi x\ maybe-eta-aux (B x) [x].
 
-      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 used i:term, i:term.
       used X (uvar _ S) :- std.mem! S X, !.
       used X (fun _ _ Bo) :- pi x\ used X (Bo x).
@@ -86,41 +81,10 @@ namespace tc {
         compile-full-aux Ty L Ty' LTy,
         compile-full-aux-close Bo Ty LTy Bo' L'.
 
-      % NOTE: when compiling t = (app [X, x, y]) and [x,y] are distinct_names,
-      %       then the coq variable has not [x,y] in scope, it is applied to
-      %       them. Note also that t is a problematic term that cannot be
-      %       exposed to the else unification algorithm.  
-      %       The solution is to build the following links:  
-      %       X =η (λa.Y a)
-      %       a |- Y a =η (λb.Z a b)
-      %       and expose a variable W at toplevel having Z has head and [x, y]
-      %       as scope
-
-      % NOTE: when compiling t = (app [X, a, x]) where a is a constant and x a
-      %       name, we build a llam link.  
-      %       The link will be: T x =L X a x  
-      %       the exposed variable in the term will be T x
-
-      % NOTE: here a combination of eta and llam:  
-      %       let t = (app [X x y, z, c, w, d]) where X is a coq var with x and
-      %       y in scope, z and w are names and c, d are constants.  
-      %       In this case, the links should be:  
-      %       X x y =η (λa.Y x y a)  
-      %       a |- Z x y a w =L (app[Y x y a, c w d])  
-      %       The returned variable is Z x y a w
-
-      % Link for beta-redex (Uvar in PF)
-      % BUILD CHAIN OF LINKS-ETA from X to V...
       % TODO: to avoid too many chain for the same var, maybe pass a list into the fold
-      compile-full-aux (app [(uvar _ Scope as V) | S] as T) L G' L'' :- !,
-        % By construction the scope of a uvar is a list of distinct name
-        std.fold-map S L compile-full-aux S' L', % LS = Links built for S
-        coq.typecheck V Ty ok,
-        split-pf S' Scope PF NPF,
-        free-names T Names,
-        tc.link.build-eta-llam-links V Scope Ty Names PF NPF L' G'' L'',
-        prune G' Names,
-        var G' G'' Names.
+      compile-full-aux (app [(uvar _ _ as V) | S]) L G' L'' :- !,
+        std.fold-map S L compile-full-aux S' L', % L' = Links built for S
+        tc.link.build-eta-llam-links (app [V|S']) L' G' L''.
 
       compile-full-aux (app L) A (app L1) A1 :- !, std.fold-map L A compile-full-aux L1 A1.
 
diff --git a/apps/tc/elpi/compile_instance.elpi b/apps/tc/elpi/compile_instance.elpi
index adb7a78e7..ac94c44bf 100644
--- a/apps/tc/elpi/compile_instance.elpi
+++ b/apps/tc/elpi/compile_instance.elpi
@@ -119,7 +119,7 @@ namespace tc {
         (pi x\ is-name x => precompile-aux is_neg_fix (B x) N' (B' x) M).
 
       precompile-aux _ (app [X|XS]) N (tc.maybe-llam-tm (app [app[X | PF] | NPF1]) Scope) (s M) :-
-        if (is-uvar X) (Sc = []) (var X _ Sc), split-pf XS Sc PF NPF, 
+        is-uvar X, split-pf XS [] PF NPF, 
         not (NPF = []), !, % else XS is a list of distinct names, i.e. `app [X|XS]` is in PF
         free-var Scope,
         std.fold-map NPF N (precompile-aux is_neg_fix) NPF1 M. 
@@ -237,27 +237,11 @@ namespace tc {
           std.fold-map NPF (pr XS L1) decompile-term-aux Tl (pr XS' L2), 
           NL = tc.link.llam Y (app [Hd|Tl]).
 
-        % Maybe-llam when H is a hole appearing in the shelved goals
-        % This happens when the instance to be compiled comes from the context
-        % Example: Goal exists (X : T1 -> T2), forall a, c (X a) -> ...
-        %            intros; eexists. (* In the context we have the instance `H: c (?X a)` *)
-        decompile-term-aux (tc.maybe-llam-tm (app[app[V | PF] | NPF] as T) S_) L G'' (pr XS' L'') :-  !,
-          var V _ Scope, !,
-          std.fold-map NPF L decompile-term-aux NPF' (pr XS' L'),
-          free-names T Names,
-          coq.typecheck V Ty ok,
-          tc.link.build-eta-llam-links V Scope Ty Names PF NPF' L' G' L'',
-          prune G'' Names,
-          var G'' G' Names.
-
-        % HO var when H is a hole appearing in the shelved goals
-        decompile-term-aux (app [V|PF] as T) (pr XS' L') G'' (pr XS' L'') :-
-          var V _ Scope, !,
-          free-names T Names,
-          coq.typecheck V Ty ok,
-          tc.link.build-eta-llam-links V Scope Ty Names PF [] L' G' L'',
-          prune G'' Names,
-          var G'' G' Names.
+        % Here we have a coq evar applied to some terms. In this case, we build
+        % eta-llam links after the decompilation of S.
+        decompile-term-aux (app [(uvar _ _ as V)|S]) PR H (pr XS L') :- !,
+          std.fold-map S PR decompile-term-aux S' (pr XS L),
+          tc.link.build-eta-llam-links (app [V|S']) L H L'.
 
         decompile-term-aux (fun Name Ty Bo) (pr XS L) (fun Name Ty' Bo') (pr XS2 L3) :- !,
           (pi x\ is-name x => decompile-term-aux (Bo x) (pr XS []) (Bo' x) (pr XS1 (L1x x))),
diff --git a/apps/tc/elpi/link.elpi b/apps/tc/elpi/link.elpi
index e0d43131a..0cadfdecd 100644
--- a/apps/tc/elpi/link.elpi
+++ b/apps/tc/elpi/link.elpi
@@ -9,28 +9,58 @@ namespace tc {
       (pi X H L Ign\ fold-map X L X [H|L] :- var X H Ign, !) => 
         fold-map T [] _ R.
 
-    % [build-eta-llam-links LHS Scope Ty Names PF NPF OldLinks NewVar NewLinks]
-    % Builds the eta/llam links at runtime for a term having the shape 
-    % `app[(uvar X Scope as V) | L]`.
-    % LHS should be V, Scope the scope of V, TODO: finish to document this...
+    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.
+
+    % [build-eta-llam-links.aux LHS Scope Ty Names PF NPF OldLinks NewVar NewLinks]
     :index(_ _ _ _ 3)
-    % TODO: the argument Ty is unused, i.e. the binders of the eta links have no type...
-    %                           LHS      Scope      Ty          Names        PF         NPF        OldLinks    NewVar
-    pred build-eta-llam-links i:term, i:list term, o:term, i:list term, i:list term, i:list term, i:list prop, o:term, o:list prop.
-    build-eta-llam-links LHS _ _       Names []  NPF OL HD [tc.link.llam T (app [LHS | NPF]) | OL] :- !,
+    pred build-eta-llam-links.aux i:term, i:list term, o:term, i:list term, i:list term, i:list term, i:list prop, o:term, o:list prop.
+    build-eta-llam-links.aux LHS _ _       Names []  NPF OL HD [llam T (app [LHS | NPF]) | OL] :- !,
       std.assert! (not (NPF = [])) "[TC] NPF List should not be empty",
       prune T Names,
       var T HD _. 
-    build-eta-llam-links LHS SC (prod _ Ty _)       _    [X] []  OL HD [tc.link.eta LHS (fun `_` Ty (x\ V x)) | OL] :- !,
+    build-eta-llam-links.aux LHS SC (prod _ Ty _)       _    [X] []  OL HD [eta LHS (fun `_` Ty (x\ V x)) | OL] :- !,
       prune V SC, var (V X) HD _.
-    build-eta-llam-links LHS SC (prod _ Ty Bo) Names [X|XS] NPF OL HD [tc.link.eta LHS (fun `_` Ty (x\ LHS' x)) | L] :- !,
+    build-eta-llam-links.aux LHS SC (prod _ Ty Bo) Names [X|XS] NPF OL HD [eta LHS (fun `_` Ty (x\ LHS' x)) | L] :- !,
     % TODO: unfold Ty if needed...
       std.append SC [X] SC',
-      prune LHS' SC, build-eta-llam-links (LHS' X) SC' (Bo X) Names XS NPF OL HD L.
-    build-eta-llam-links LHS SC Ty Names ([_|_] as PF) NPF OL HD L :-
+      prune LHS' SC, build-eta-llam-links.aux (LHS' X) SC' (Bo X) Names XS NPF OL HD L.
+    build-eta-llam-links.aux LHS SC Ty Names ([_|_] as PF) NPF OL HD L :-
       Ty' = prod _ _ _, coq.unify-eq Ty Ty' ok, !,
-      build-eta-llam-links LHS SC Ty' Names PF NPF OL HD L.
-
+      build-eta-llam-links.aux LHS SC Ty' Names PF NPF OL HD L.
+    
+    % [build-eta-llam-links T OldLinks X NewLinks]  
+    % T = app[(uvar _ Scope) | S] this term is problematic and asks for the
+    % creation of eta- and/or llam-links. Below some examples:
+
+    % eta: when compiling t = (app [X, x, y]) and [x,y] are distinct_names, then
+    %     the coq variable has not [x,y] in scope: it is applied to them.  
+    %     The solution is to build the following links:  
+    %     NewLinks = [X =η (λa.Y a),     a |- Y a =η (λb.Z a b)]
+    %     and the exposed variable is G, given by `var G Z [x, y]`
+
+    % llam: when compiling t = (app [X, a, x]) where a is a constant and x a
+    %       name, we build a llam link.  
+    %       The link will be: NewLinks ] = [T x =L X a x]  
+    %       and the exposed variable is G, given by `var G T [x]`
+
+    % eta-llam: here a combination of eta and llam:  
+    %       let t = (app [X x y, z, c, w, d]) where X is a coq var with x and y
+    %       in scope, z and w are names and c, d are constants.  
+    %       In this case, the links should be:  
+    %       NewLinks = [X x y =η (λa.Y x y a),   a |- Z x y a w =L (app[Y x y a, c w d])]  
+    %       and the exposed variable is G, given by `var Z T [x, y, z, w]`  
+    pred build-eta-llam-links i:term, i:list prop, o:term, o:list prop.
+    build-eta-llam-links (app[(uvar _ Scope as V) | S] as T) Links G NewLinks :- !,
+      coq.typecheck V Ty ok,
+      split-pf S Scope PF NPF,
+      free-names T Names,
+      build-eta-llam-links.aux V Scope Ty Names PF NPF Links LhsHd NewLinks,
+      prune G Names,
+      var G LhsHd Names.
+    build-eta-llam-links T _ _ _ :- coq.error "[TC] invalid call to build-eta-llam-links:" T.
 
     %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
     % ETA LINK                                                                 %
diff --git a/apps/tc/tests/test.v b/apps/tc/tests/test.v
index 96e8fd442..228748ba7 100644
--- a/apps/tc/tests/test.v
+++ b/apps/tc/tests/test.v
@@ -596,7 +596,7 @@ Module CoqUvar4.
     tc.precomp.instance {{c1 (fun x y => lp:X (lp:A x y) y)}} C _ _ _,
     Expected = app [{{c1}}, tc.maybe-eta-tm (fun _ _ Body1) _],
     Body1 = (x\ tc.maybe-eta-tm (fun _ _ (Body2 x)) [x]),
-    Body2 = (x\y\ tc.maybe-llam-tm (app [app [X], (Y x y), y]) [y,x]),
+    Body2 = (x\y\ app [X, (Y x y), y]),
     std.assert! (C = Expected) "[TC] invalid compilation".
   }}.