diff options
| author | Matej Kosik | 2015-11-10 09:11:50 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2015-12-10 09:35:19 +0100 |
| commit | 32bd14114d5137b917601092730469db569d6385 (patch) | |
| tree | b416c7da024ad1401da727dbf22cdd1a8a6a8aae /kernel/nativecode.mli | |
| parent | 5e48f1aafb45d1c883e32e13a8458979663b04fb (diff) | |
PROPOSITION: Added an explicit definition of the notation for enriching the global environment (we use throughout the document)
Diffstat (limited to 'kernel/nativecode.mli')
0 files changed, 0 insertions, 0 deletions