diff options
| author | Pierre-Marie Pédrot | 2020-02-09 12:27:30 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-02-09 12:27:30 +0100 |
| commit | d96e6bc44437de5c27ff26b6a75b92904e4e7887 (patch) | |
| tree | f9623dfdbdd42233767fbadf3bd67d7a69a678c8 /kernel/declarations.ml | |
| parent | da340c202c3348025942665d45703b5a093d255c (diff) | |
| parent | 3e460f77c1777ce1a8d393f2335fd7f4b4fe924f (diff) | |
Merge PR #11550: Fixing wrong comments in context.ml
Reviewed-by: ppedrot
Diffstat (limited to 'kernel/declarations.ml')
0 files changed, 0 insertions, 0 deletions