fix documentation

Author: gares

coq-builtin.elpi

@@ -1374,12 +1374,13 @@ external pred coq.elaborate-ty-skeleton i:term, o:sort, o:term,
 % Flags for lazy, cbv, ... reductions
 kind coq.redflag type.
 type coq.redflags.beta coq.redflag.
-type coq.redflags.delta coq.redflag.
+type coq.redflags.delta coq.redflag. % if set then coq.redflags.const disables unfolding
 type coq.redflags.match coq.redflag.
 type coq.redflags.fix coq.redflag.
 type coq.redflags.cofix coq.redflag.
 type coq.redflags.zeta coq.redflag.
-type coq.redflags.const constant -> coq.redflag.
+type coq.redflags.const constant ->
+                        coq.redflag. % enable/disable unfolding
 
 % Set of flags for lazy, cbv, ... reductions
 typeabbrev coq.redflags (ctype "coq.redflags").

src/coq_elpi_builtins.ml

@@ -595,7 +595,7 @@ let reduction_kind = let open API.AlgebraicData in let open CClosure.RedFlags in
     K ("coq.redflags.beta", "",N,
       B fBETA,
       M (fun ~ok ~ko x -> if x = fBETA then ok else ko ()));
-    K ("coq.redflags.delta", "",N,
+    K ("coq.redflags.delta", "if set then coq.redflags.const disables unfolding",N,
       B fDELTA,
       M (fun ~ok ~ko x -> if x = fDELTA then ok else ko ()));
     K ("coq.redflags.match", "",N,
@@ -610,7 +610,7 @@ let reduction_kind = let open API.AlgebraicData in let open CClosure.RedFlags in
     K ("coq.redflags.zeta", "",N,
       B fZETA,
       M (fun ~ok ~ko x -> if x = fZETA then ok else ko ()));
-    K("coq.redflags.const","",A(constant,N),
+    K("coq.redflags.const","enable/disable unfolding",A(constant,N),
       B (function Constant x -> fCONST x | Variable x -> fVAR x),
       M (fun ~ok ~ko x -> nYI "readback for coq.redflags.const"));
   ]