diff options
| author | Gaëtan Gilbert | 2020-07-22 14:11:09 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-07-22 14:11:09 +0200 |
| commit | 974401d5dc6164241e0575dc87f1db43f183f968 (patch) | |
| tree | a82db4d27c2759a67ca55e68365ffed52a6f623e /kernel/nativelambda.mli | |
| parent | 56fd98a932f2700a63fe701bb71533fb48d6d06b (diff) | |
Clarify Global.env usage in ppvernac
Diffstat (limited to 'kernel/nativelambda.mli')
0 files changed, 0 insertions, 0 deletions