code clean

apps/tc/elpi/tc_aux.elpi

@@ -106,20 +106,19 @@ 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 make-tc.aux i:bool, i:prop, i:list prop, o:prop.
+make-tc.aux _ Head [] Head.
+make-tc.aux tt Head Body (Head :- Body).
+make-tc.aux ff Head Body (Body => Head).
+
 pred make-tc i:term, i:term, i:list prop, i:bool, o:prop.
-make-tc Ty Inst Hyp IsPositive Clause :-
+make-tc Ty Inst Body IsPositive Clause :-
   coq.safe-dest-app Ty HD TL,
   get-TC-of-inst-type HD TC,
   gref->pred-name TC TC_Str,
   std.append TL [Inst] Args, 
-  coq.elpi.predicate TC_Str Args Q,
-  if (IsPositive = tt)
-  (if2 (Hyp = []) (Clause = Q) 
-      (Hyp = [Hd]) (Clause = (Q :- Hd)) 
-      (Clause = (Q :- Hyp)))
-  (if2 (Hyp = []) (Clause = Q) 
-    (Hyp = [Hd]) (Clause = (Hd => Q)) 
-    (Clause = (Hyp => Q))).
+  coq.elpi.predicate TC_Str Args Head,
+  make-tc.aux IsPositive Head Body Clause.
 
 pred unwrap-prio i:tc-priority, o:int.
 unwrap-prio (tc-priority-given Prio) Prio.