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