summaryrefslogtreecommitdiff
path: root/compiler/dune-project
diff options
context:
space:
mode:
authorSon Ho2023-07-05 15:17:58 +0200
committerSon Ho2023-07-05 15:17:58 +0200
commit5ca36bfc50083a01af2b7ae5f75993a520757ef5 (patch)
tree11660b73a27ad2e0807a18ac9286a1e87c560050 /compiler/dune-project
parentc07721dedb2cfe4c726c42606e623395cdfe5b80 (diff)
Simplify the names used in Primitives.lean
Diffstat (limited to '')
0 files changed, 0 insertions, 0 deletions