update builtins

Author: FissoreD

builtin-doc/coq-builtin.elpi

@@ -558,8 +558,8 @@ external pred coq.version o:string, o:int, o:int, o:int.
 
 % To make the API more precise we use different data types for the names
 % of global objects.
-% Note: [ctype \"bla\"] is an opaque data type and by convention it is
-% written [@bla].
+% Note: [ctype "bla"] is an opaque data type and by convention it is written
+% [@bla].
 
 % Global constant name
 typeabbrev constant (ctype "constant").

builtin-doc/elpi-builtin.elpi

@@ -449,6 +449,9 @@ pred ignore-failure! i:prop.
 ignore-failure! P :- P, !.
 ignore-failure! _.
 
+pred once i:prop.
+once P :- P, !.
+
 % [assert! C M] takes the first success of C or fails with message M 
 pred assert! i:prop, i:string.
 assert! Cond Msg :- (Cond ; fatal-error-w-data Msg Cond), !.