summaryrefslogtreecommitdiff
path: root/src/PureToExtract.ml
diff options
context:
space:
mode:
authorSon Ho2022-02-01 19:56:38 +0100
committerSon Ho2022-02-01 19:56:38 +0100
commit5faf86a5718daf2030d77a8e8e1b321ffb13913d (patch)
treedece421bd8c2d8ee2cf9c7dec715a1de49e18e45 /src/PureToExtract.ml
parent1416493e000d2eec1541ae7c4077a6c1ae7870c1 (diff)
Make a minor modification to ExtractToFStar.extract_type_def_enum_body
Diffstat (limited to '')
0 files changed, 0 insertions, 0 deletions