aboutsummaryrefslogtreecommitdiff
path: root/engine/evd.ml
diff options
context:
space:
mode:
authorcoqbot-app[bot]2020-08-31 12:09:18 +0000
committerGitHub2020-08-31 12:09:18 +0000
commitdaca83946ed5a001f2461fefa787a80f7dcdea01 (patch)
tree0a746f4f5496290ca18c5d92d57cb7d3a9c89065 /engine/evd.ml
parentb4ff2af4f43a2e0ba40c7f8a6260da1c75859045 (diff)
parent8262041215c9bc3d13e768b1c422b52005083e85 (diff)
Merge PR #12875: Further extensions of About wrt Arguments and renaming
Reviewed-by: SkySkimmer Ack-by: herbelin
Diffstat (limited to 'engine/evd.ml')
0 files changed, 0 insertions, 0 deletions