diff --git a/builtin-doc/elpi-builtin.elpi b/builtin-doc/elpi-builtin.elpi
index 8ad5cec6f..cf2bb7420 100644
--- a/builtin-doc/elpi-builtin.elpi
+++ b/builtin-doc/elpi-builtin.elpi
@@ -31,7 +31,7 @@ kind string type.
 kind float type.
 
 
-external symbol (;) prop -> prop -> prop.
+external symbol (;) (pred) -> (pred) -> (pred).
 
 (A ; _) :- A.
 
@@ -39,7 +39,7 @@ external symbol (;) prop -> prop -> prop.
 
 external symbol (:-)  : (func) -> (func) -> (func) = "core".
 
-external symbol (:-)  : (func) -> list prop -> (func) = "core".
+external symbol (:-)  : (func) -> list (pred) -> (func) = "core".
 
 external symbol (,)   : variadic (func) (func).
 
@@ -47,13 +47,13 @@ external symbol uvar  : A = "core".
 
 external symbol (as)  : A -> A -> A = "core".
 
-external symbol (=>)  : prop -> (func) -> (func) = "core".
+external symbol (=>)  : (pred) -> (func) -> (func) = "core".
 
-external symbol (=>)  : list prop -> (func) -> (func) = "core".
+external symbol (=>)  : list (pred) -> (func) -> (func) = "core".
 
-external symbol (==>) : prop -> (func) -> (func).
+external symbol (==>) : (pred) -> (func) -> (func).
 
-external symbol (==>) : list prop -> (func) -> (func).
+external symbol (==>) : list (pred) -> (func) -> (func).
 
 %  -- Control --
 
@@ -428,12 +428,12 @@ external func open_safe safe -> list A.
 
 % [if C T E] picks the first success of C then runs T (never E).
 % if C has no success it runs E.
-func if prop, (func), (func).
+func if (pred), (func), (func).
 if B T _ :- B, !, T.
 if _ _ E :- E.
 
 % [if2 C1 B1 C2 B2 E] like if but with 2 then branches (and one else branch).
-func if2 prop, (func), prop, (func), (func).
+func if2 (pred), (func), (pred), (func), (func).
 if2 G1 P1 _  _  _ :- G1, !, P1.
 if2 _  _  G2 P2 _ :- G2, !, P2.
 if2 _  _  _  _  E :- !, E. 
@@ -496,7 +496,7 @@ assert-ok! Cond Msg :- Cond Diagnostic, !, (Diagnostic = ok ; Diagnostic = error
 assert-ok! _ Msg :- fatal-error-w-data Msg "no diagnostic returned".
 
 % [spy P] traces the call to P, printing all success and the final failure
-pred spy i:prop.
+pred spy (pred).
 spy P :- trace.counter "run" NR, if (not(NR = 0)) (debug-print "run=" NR) true,
          debug-print "----<<---- enter: " P,
          P,
@@ -537,7 +537,7 @@ func append list A, list A -> list A.
 append [X|XS] L [X|L1] :- append XS L L1 .
 append [] L L .
 
-pred appendR o:list A, o:list A, o:list A.
+pred appendR -> list A, list A, list A.
 appendR [] L L.
 appendR [X|XS] L [X|L1] :- appendR XS L L1.
 
@@ -631,14 +631,14 @@ nth N _ _ :- N < 0, !, fatal-error "nth got a negative index".
 nth _ _ _ :- fatal-error "nth run out of list items".
 
 % [lookup L K V] sees L as a map from K to V
-pred lookup i:list (pair A B), i:A, o:B.
+pred lookup list (pair A B), A -> B.
 lookup [pr X Y|_] X Y.
-lookup [_|LS]       X Y :- lookup LS X Y.
+lookup [_|LS]     X Y :- lookup LS X Y.
 
 % [lookup! L K V] sees L as a map from K to V, stops at the first binding
 func lookup! list (pair A B), A -> B.
 lookup! [pr X Y|_] X Y :- !.
-lookup! [_|LS]       X Y :- lookup! LS X Y.
+lookup! [_|LS]     X Y :- lookup! LS X Y.
 
 % [mem! L X] succeeds once if X occurs inside L 
 func mem! list A, A ->.
@@ -646,19 +646,19 @@ mem! [X|_] X :- !.
 mem! [_|L] X :- mem! L X.
 
 % [mem L X] succeeds every time if X occurs inside L 
-pred mem i:list A, o:A.
+pred mem list A -> A.
 mem [X|_] X.
 mem [_|L] X :- mem L X.
 
-func exists! list A, (pred i:A) ->.
+func exists! list A, (pred A).
 exists! [X| _] P :- P X, !.
 exists! [_|XS] P :- exists! XS P. 
 
-pred exists i:list A, i:(pred i:A).
+pred exists list A, (pred A).
 exists [X|_] P :- P X.
 exists [_|L] P :- exists L P.
 
-pred exists2 i:list A, i:list B, i:(pred i:A, i:B).
+pred exists2 list A, list B, (pred A, B).
 exists2 [] [_|_] _ :- fatal-error "exists2 on lists of different length".
 exists2 [_|_] [] _ :- fatal-error "exists2 on lists of different length".
 exists2 [X|_] [Y|_] P :- P X Y.
@@ -683,7 +683,7 @@ filter []    _ [].
 filter [X|L] P R :- if (P X) (R = X :: L1) (R = L1), filter L P L1.
 
 :index (1)
-func partition list A, (pred i:A) -> list A, list A.
+func partition list A, (pred A) -> list A, list A.
 partition [] _ [] [].
 partition [X|XS] P [X|R] L :- P X, !, partition XS P R L.
 partition [X|XS] P R [X|L] :- partition XS P R L.
@@ -747,13 +747,13 @@ pred do-ok! o:diagnostic, i:list (pred o:diagnostic).
 do-ok! ok [].
 do-ok! S [P|PS] :- P S0, !, if (S0 = ok) (do-ok! S PS) (S = S0).
 
-pred lift-ok i:prop, i:string, o:diagnostic.
+pred lift-ok (pred), string -> diagnostic.
 lift-ok P Msg R :- (P, R = ok; R = error Msg).
 
 func spy-do! list prop.
 spy-do! L :- map L (x\y\y = spy x) L1, do! L1.
 
-func while-ok-do! diagnostic, list (pred o:diagnostic) -> diagnostic.
+func while-ok-do! diagnostic, list (pred -> diagnostic) -> diagnostic.
 while-ok-do! (error _ as E) _ E.
 while-ok-do! ok [] ok.
 while-ok-do! ok [P|PS] R :- P C, !, while-ok-do! C PS R.
@@ -1071,28 +1071,28 @@ external func std.loc.set.partition std.loc.set,
 
 #line 1 "builtin_map.elpi"
 kind std.map type -> type -> type.
-type std.map std.map.private.map K V -> (pred i:K, i:K, o:cmp) -> std.map K V.
+type std.map std.map.private.map K V -> (func K, K -> cmp) -> std.map K V.
 
 namespace std.map {
 
 % [make Eq Ltn M] builds an empty map M where keys are compared using Eq and Ltn
-pred make i:(pred i:K, i:K, o:cmp), o:std.map K V.
+func make (func K, K -> cmp) -> std.map K V.
 make Cmp (std.map private.empty Cmp).
 
 % [find K M V] looks in M for the value V associated to K
-pred find i:K, i:std.map K V, o:V.
+func find K, std.map K V -> V.
 find K (std.map M Cmp) V :- private.find M Cmp K V.
 
 % [add K V M M1] M1 is M where K is bound to V
-pred add i:K, i:V, i:std.map K V, o:std.map K V.
+func add K, V, std.map K V -> std.map K V.
 add K V (std.map M Cmp) (std.map M1 Cmp) :- private.add M Cmp K V M1.
 
 % [remove K M M1] M1 is M where K is unbound
-pred remove i:K, i:std.map K V, o:std.map K V.
+func remove K, std.map K V -> std.map K V.
 remove K (std.map M Cmp) (std.map M1 Cmp) :- private.remove M Cmp K M1.
 
 % [bindings M L] L is the key-value pairs in increasing order
-pred bindings i:std.map K V, o:list (pair K V).
+func bindings std.map K V -> list (pair K V).
 bindings (std.map M _) L :- private.bindings M [] L.
 
 namespace private {
@@ -1102,14 +1102,14 @@ kind map type -> type -> type.
 type empty map K V.
 type node map K V -> K -> V -> map K V -> int -> map K V.
 
-pred height i:map K V, o:int.
+func height map K V -> int.
 height empty 0.
 height (node _ _ _ _ H) H.
 
-pred create i:map K V, i:K, i:V, i:map K V, o:map K V.
+func create map K V, K, V, map K V -> map K V.
 create L K V R (node L K V R H) :- H is {std.max {height L} {height R}} + 1.
 
-pred bal i:map K V, i:K, i:V, i:map K V, o:map K V.
+func bal map K V, K, V, map K V -> map K V.
 bal L K V R T :-
   height L HL,
   height R HR,
@@ -1117,7 +1117,7 @@ bal L K V R T :-
   HR2 is HR + 2,
   bal.aux HL HR HL2 HR2 L K V R T.
 
-pred bal.aux i:int, i:int, i:int, i:int, i:map K V, i:K, i:V, i:map K V, o:map K V.
+func bal.aux int, int, int, int, map K V, K, V, map K V -> map K V.
 bal.aux HL _ _ HR2 (node LL LV LD LR _) X D R T :-
   HL > HR2, {height LL} >= {height LR}, !,
   create LL LV LD {create LR X D R} T.
@@ -1132,48 +1132,48 @@ bal.aux _ HR HL2 _ L X D (node (node RLL RLV RLD RLR _) RV RD RR _) T :-
   create {create L X D RLL} RLV RLD {create RLR RV RD RR} T.
 bal.aux _ _ _ _ L K V R T :- create L K V R T.
 
-pred add i:map K V, i:(pred i:K, i:K, o:cmp), i:K, i:V, o:map K V.
+func add map K V, (func K, K -> cmp), K, V -> map K V.
 add empty _ K V T :- create empty K V empty T.
 add (node _ X _ _ _ as M) Cmp X1 XD M1 :- Cmp X1 X E, add.aux E M Cmp X1 XD M1.
 
-pred add.aux i:cmp, i:map K V, i:(pred i:K, i:K, o:cmp), i:K, i:V, o:map K V.
+func add.aux cmp, map K V, (func K, K -> cmp), K, V -> map K V.
 add.aux eq (node L _ _ R H) _   X XD T :- T = node L X XD R H. 
 add.aux lt (node L V D R _) Cmp X XD T :- bal {add L Cmp X XD} V D R T.
 add.aux gt (node L V D R _) Cmp X XD T :- bal L V D {add R Cmp X XD} T.
 
-pred find i:map K V, i:(pred i:K, i:K, o:cmp), i:K, o:V.
+func find map K V, (func K, K -> cmp), K -> V.
 find (node L K1 V1 R _) Cmp K V :- Cmp K K1 E, find.aux E Cmp L R V1 K V.
 
-pred find.aux i:cmp, i:(pred i:K, i:K, o:cmp), i:map K V, i:map K V, i:V, i:K, o:V.
+func find.aux cmp, (func K, K -> cmp), map K V, map K V, V, K -> V.
 find.aux eq _   _ _ V _ V.
 find.aux lt Cmp L _ _ K V :- find L Cmp K V.
 find.aux gt Cmp _ R _ K V :- find R Cmp K V.
 
-pred remove-min-binding i:map K V, o:map K V.
+func remove-min-binding map K V -> map K V.
 remove-min-binding (node empty _ _ R _) R :- !.
 remove-min-binding (node L V D R _) X :- bal {remove-min-binding L} V D R X.
 
-pred min-binding i:map K V, o:K, o:V.
+func min-binding map K V -> K, V.
 min-binding (node empty V D _ _) V D :- !.
 min-binding (node L _ _ _ _) V D :- min-binding L V D.
 
-pred merge i:map K V, i:map K V, o:map K V.
+func merge map K V, map K V -> map K V.
 merge empty X X :- !.
 merge X empty X :- !.
 merge M1 M2 R :-
   min-binding M2 X D,
   bal M1 X D {remove-min-binding M2} R.
 
-pred remove i:map K V, i:(pred i:K, i:K, o:cmp), i:K, o:map K V.
+func remove map K V, (func K, K -> cmp), K -> map K V.
 remove empty _ _ empty :- !.
 remove (node L V D R _) Cmp X M :- Cmp X V E, remove.aux E Cmp L R V D X M.
 
-pred remove.aux i:cmp, i:(pred i:K, i:K, o:cmp), i:map K V, i:map K V, i:K, i:V, i:K, o:map K V.
+func remove.aux cmp, (func K, K -> cmp), map K V, map K V, K, V, K -> map K V.
 remove.aux eq _   L R _ _ _ M :- merge L R M.
 remove.aux lt Cmp L R V D X M :- bal {remove L Cmp X} V D R M.
 remove.aux gt Cmp L R V D X M :- bal L V D {remove R Cmp X} M.
 
-pred bindings i:map K V, i:list (pair K V), o:list (pair K V).
+func bindings map K V, list (pair K V) -> list (pair K V).
 bindings empty X X.
 bindings (node L V D R _) X X1 :-
   bindings L [pr V D|{bindings R X}] X1.
@@ -1185,31 +1185,31 @@ bindings (node L V D R _) X X1 :-
 
 #line 1 "builtin_set.elpi"
 kind std.set type -> type.
-type std.set std.set.private.set E -> (pred i:E, i:E, o:cmp) -> std.set E.
+type std.set std.set.private.set E -> (func E, E -> cmp) -> std.set E.
 
 namespace std.set {
 
 % [make Eq Ltn M] builds an empty set M where keys are compared using Eq and Ltn
-pred make i:(pred i:E, i:E, o:cmp), o:std.set E.
+func make (func E, E -> cmp) -> std.set E.
 make Cmp (std.set private.empty Cmp).
 
 % [mem E M] looks if E is in M
-pred mem i:E, i:std.set E.
+func mem E, std.set E.
 mem E (std.set M Cmp):- private.mem M Cmp E.
 
 % [add E M M1] M1 is M + {E}
-pred add i:E, i:std.set E, o:std.set E.
+func add E, std.set E -> std.set E.
 add E (std.set M Cmp) (std.set M1 Cmp) :- private.add M Cmp E M1.
 
 % [remove E M M1] M1 is M - {E}
-pred remove i:E, i:std.set E, o:std.set E.
+func remove E, std.set E -> std.set E.
 remove E (std.set M Cmp) (std.set M1 Cmp) :- private.remove M Cmp E M1.
 
 % [cardinal S N] N is the number of elements of S
-pred cardinal i:std.set E, o:int.
+func cardinal std.set E -> int.
 cardinal (std.set M _) N :- private.cardinal M N.
 
-pred elements i:std.set E, o:list E.
+func elements std.set E -> list E.
 elements (std.set M _) L :- private.elements M [] L.
 
 namespace private {
@@ -1219,14 +1219,14 @@ kind set type -> type.
 type empty set E.
 type node set E -> E -> set E -> int -> set E.
 
-pred height i:set E, o:int.
+func height set E -> int.
 height empty 0.
 height (node _ _ _ H) H.
 
-pred create i:set E, i:E, i:set E, o:set E.
+func create set E, E, set E -> set E.
 create L E R (node L E R H) :- H is {std.max {height L} {height R}} + 1.
 
-pred bal i:set E, i:E, i:set E, o:set E.
+func bal set E, E, set E -> set E.
 bal L E R T :-
   height L HL,
   height R HR,
@@ -1234,7 +1234,7 @@ bal L E R T :-
   HR2 is HR + 2,
   bal.aux HL HR HL2 HR2 L E R T.
 
-pred bal.aux i:int, i:int, i:int, i:int, i:set E, i:E, i:set E, o:set E.
+func bal.aux int, int, int, int, set E, E, set E -> set E.
 bal.aux HL _ _ HR2 (node LL LV LR _) X R T :-
   HL > HR2, {height LL} >= {height LR}, !,
   create LL LV {create LR X R} T.
@@ -1249,52 +1249,52 @@ bal.aux _ HR HL2 _ L X (node (node RLL RLV RLR _) RV RR _) T :-
   create {create L X RLL} RLV {create RLR RV RR} T.
 bal.aux _ _ _ _ L E R T :- create L E R T.
 
-pred add i:set E, i:(pred i:E, i:E, o:cmp), i:E, o:set E.
+func add set E, (func E, E -> cmp), E -> set E.
 add empty _ E T :- create empty E empty T.
 add (node L X R H) Cmp X1 S :- Cmp X1 X E, add.aux E Cmp L R X X1 H S.
 
-pred add.aux i:cmp, i:(pred i:E, i:E, o:cmp), i:set E, i:set E, i:E, i:E, i:int, o:set E.
+func add.aux cmp, (func E, E -> cmp), set E, set E, E, E, int -> set E.
 add.aux eq _   L R X _ H (node L X R H).
 add.aux lt Cmp L R E X _ T :- bal {add L Cmp X} E R T.
 add.aux gt Cmp L R E X _ T :- bal L E {add R Cmp X} T.
 
-pred mem i:set E, i:(pred i:E, i:E, o:cmp), i:E.
+func mem set E, (func E, E -> cmp), E.
 mem (node L K R _) Cmp E :- Cmp E K O, mem.aux O Cmp L R E.
-mem.aux eq _ _ _ _.
 
-pred mem.aux i:cmp, i:(pred i:E, i:E, o:cmp), i:set E, i:set E, i:E.
+func mem.aux cmp, (func E, E -> cmp), set E, set E, E.
+mem.aux eq _ _ _ _.
 mem.aux lt Cmp L _ E :- mem L Cmp E.
 mem.aux gt Cmp _ R E :- mem R Cmp E.
 
-pred remove-min-binding i:set E, o:set E.
+func remove-min-binding set E -> set E.
 remove-min-binding (node empty _ R _) R :- !.
 remove-min-binding (node L E R _) X :- bal {remove-min-binding L} E R X.
 
-pred min-binding i:set E, o:E.
+func min-binding set E -> E.
 min-binding (node empty E _ _) E :- !.
 min-binding (node L _ _ _) E :- min-binding L E.
 
-pred merge i:set E, i:set E, o:set E.
+func merge set E, set E -> set E.
 merge empty X X :- !.
 merge X empty X :- !.
 merge M1 M2 R :-
   min-binding M2 X,
   bal M1 X {remove-min-binding M2} R.
 
-pred remove i:set E, i:(pred i:E, i:E, o:cmp), i:E, o:set E.
+func remove set E, (func E, E -> cmp), E -> set E.
 remove empty _ _ empty.
 remove (node L E R _) Cmp X M :- Cmp X E O, remove.aux O Cmp L R E X M.
 
-pred remove.aux i:cmp, i:(pred i:E, i:E, o:cmp), i:set E, i:set E, i:E, i:E, o:set E.
+func remove.aux cmp, (func E, E -> cmp), set E, set E, E, E -> set E.
 remove.aux eq _   L R _ _ M :- merge L R M.
 remove.aux lt Cmp L R E X M :- bal {remove L Cmp X} E R M.
 remove.aux gt Cmp L R E X M :- bal L E {remove R Cmp X} M.
 
-pred cardinal i:set E, o:int.
+func cardinal set E -> int.
 cardinal empty 0.
 cardinal (node L _ R _) N :- N is {cardinal L} + 1 + {cardinal R}.
 
-pred elements i:set E, i:list E, o:list E.
+func elements set E, list E -> list E.
 elements empty X X.
 elements (node L E R _) Acc X :-
   elements L [E|{elements R Acc}] X.
@@ -1439,7 +1439,7 @@ external func open_string string -> in_stream.
 % [lookahead InStream NextChar] peeks one byte from InStream
 external func lookahead in_stream -> string.
 
-pred printterm i:out_stream, i:A.
+pred printterm out_stream, A.
 
 printterm S T :- term_to_string T T1, output S T1.
 
diff --git a/tests/test_detcheck.v b/tests/test_detcheck.v
new file mode 100644
index 000000000..450e8c8b7
--- /dev/null
+++ b/tests/test_detcheck.v
@@ -0,0 +1,18 @@
+From elpi Require Import elpi.
+
+Elpi Command test.
+Elpi Db foo lp:{{/*(*/
+  pred test o:pstring.
+/*)*/}}.
+Elpi File buggy_inline lp:{{/*(*/
+kind f type -> type.
+kind s type.
+typeabbrev pstring (f s).
+/*)*/}}.
+Fail Elpi Accumulate foo File buggy_inline.
+(* Elpi Accumulate Db foo.
+Elpi Query lp:{{/*(*/
+  coq.string->pstring "x" Primx,
+  X = test Primx,
+  coq.elpi.accumulate _ "foo" (clause _ _ X).
+/*)*/}}. *)