aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
authorPierre Roux2019-02-11 10:13:05 +0100
committerPierre Roux2019-02-11 10:13:05 +0100
commit80a6828ede8441380f42f463521282e4b60d3193 (patch)
tree650a64216cc82f1e5c29fef80485d8ddc5c962c5 /dev
parentaa66e4b3e58699db5af904e14247c73744398732 (diff)
[coqdoc] Add the From keyword
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions