aboutsummaryrefslogtreecommitdiff
path: root/lib/xml_datatype.mli
diff options
context:
space:
mode:
authorcoqbot-app[bot]2021-04-25 18:02:47 +0000
committerGitHub2021-04-25 18:02:47 +0000
commit6683de2eaa499bd269e75d064a1674d5e4d10d34 (patch)
tree18c03d4b603a74b20a2935c4a12ed72d505f44a1 /lib/xml_datatype.mli
parentd9e9a63f9f49768eee8b239812365ad1115b964f (diff)
parent9caadc38de0e1c7b3362081da9482fc4455220a7 (diff)
Merge PR #13674: Enhance the performance of the move tacticHEADmaster
Reviewed-by: herbelin
Diffstat (limited to 'lib/xml_datatype.mli')
0 files changed, 0 insertions, 0 deletions