summaryrefslogtreecommitdiff
path: root/tests/misc/External.Opaque.fsti
diff options
context:
space:
mode:
authorSon Ho2022-04-20 15:59:54 +0200
committerSon Ho2022-04-20 15:59:54 +0200
commit0d4e85006d06c51194db17a08055c00ee830124a (patch)
treed8dd684f1323de427e21e894ad951fb3fa7be719 /tests/misc/External.Opaque.fsti
parent808afaa654d41257373df2379630bc72542b970b (diff)
Introduce mdplace to link meta information about the given back values
to the information about the input arguments
Diffstat (limited to '')
0 files changed, 0 insertions, 0 deletions