diff options
| author | Théo Zimmermann | 2020-12-29 18:58:46 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2020-12-29 19:52:15 +0100 |
| commit | 627dcd739d67fdc4535af9ca0e36e65b3714f477 (patch) | |
| tree | e364ea9b006d56f1ae1d28b21aa642bcb5d59c7b /kernel/type_errors.mli | |
| parent | 942fb01934b02181fd3a88d80fc870f8d4900d2c (diff) | |
[refman] Clarify meaning of goal in documentation of instantiate.
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions