Skip to content

Commit 0a43023

Browse files
Tragicusgares
andauthored
improve primitive-projection? doc
Co-authored-by: Enrico Tassi <[email protected]>
1 parent b587ac3 commit 0a43023

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

src/rocq_elpi_builtins.ml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2364,7 +2364,7 @@ denote the same x as before.|};
23642364
InOut(B.ioarg projection, "Projection",
23652365
InOut(B.ioarg constant, "Compatibility constant",
23662366
Out(int, "Index",
2367-
Read(global, "Relates a primitive projection to its compatibility constant and its index in the record.")))),
2367+
Read(global, "Relates a primitive projection to its compatibility constant. Index is set to the constructor argument extracted by the projection (starting from 0).")))),
23682368
(fun p c _ ~depth coq_context _ _ ->
23692369
match p, c with
23702370
| _, Data (Variable c) -> raise No_clause

0 commit comments

Comments
 (0)