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