diff options
| author | Hugo Herbelin | 2017-08-10 17:10:48 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2018-02-20 10:03:03 +0100 |
| commit | 9324dcf528f16be420b08c376a6580c8987f50fd (patch) | |
| tree | 21eda2f66226c0f9da6a9e6efd623048c4bb983d /kernel/cbytecodes.ml | |
| parent | 6b9a9124d3bd24fe9305df613547139f6f609c60 (diff) | |
Using name given by user to name a 'pat, if any.
This works for contexts in Definition and co, but not yet for "fun" and co.
Diffstat (limited to 'kernel/cbytecodes.ml')
0 files changed, 0 insertions, 0 deletions