diff options
| author | Pierre Letouzey | 2015-12-06 12:41:55 +0100 |
|---|---|---|
| committer | Pierre Letouzey | 2015-12-12 18:51:37 +0100 |
| commit | a275da6e67b91d9ccae0a952eb1feab2e122076e (patch) | |
| tree | ea1c0bc8bcbc19ca67090de59dc867882c43a7f2 /plugins/extraction | |
| parent | ec5455d7351c05a58ae99d5a300dc8576f8c9360 (diff) | |
Extraction: documentation of the new option Unset Extraction SafeImplicits
Diffstat (limited to 'plugins/extraction')
0 files changed, 0 insertions, 0 deletions