diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-07-04 17:00:48 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-07-26 15:11:14 +0200 |
| commit | 9961577dfbb93f0b691c355ba99822665def037f (patch) | |
| tree | 11f7fc112285f2f64118441937f47cf4d1236c29 /kernel/safe_typing.ml | |
| parent | 4457e6d75affd20c1c13c0d798c490129525bcb5 (diff) | |
Using a record type for Cooking.result.
Diffstat (limited to 'kernel/safe_typing.ml')
0 files changed, 0 insertions, 0 deletions