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/float64_common.ml | |
| parent | 942fb01934b02181fd3a88d80fc870f8d4900d2c (diff) | |
[refman] Clarify meaning of goal in documentation of instantiate.
Diffstat (limited to 'kernel/float64_common.ml')
0 files changed, 0 insertions, 0 deletions