diff options
| author | David A. Dalrymple | 2019-01-23 18:19:28 -0500 |
|---|---|---|
| committer | GitHub | 2019-01-23 18:19:28 -0500 |
| commit | 8d6d5e3107f2b5f075d7daca69eeaf5fbbd7d0f4 (patch) | |
| tree | dc5fa17d8837dcea6f62b6e75d3addeff2108142 /kernel/cbytecodes.ml | |
| parent | f5241b99bb15f019eb629a7f24f2993f011e7e06 (diff) | |
Clarify meaning of Primitive Projections
The previous language makes it seem as if record parameters are automatically set as implicit for the projection functions, but (per discussion with @jasongross) the omission of parameters from primitive projection only takes effect in Coq's internal AST.
Diffstat (limited to 'kernel/cbytecodes.ml')
0 files changed, 0 insertions, 0 deletions