diff options
| author | Hugo Herbelin | 2020-02-08 15:33:22 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-02-08 15:33:22 +0100 |
| commit | da340c202c3348025942665d45703b5a093d255c (patch) | |
| tree | 0d408e010ba5bb28fcd3726f625bdfecfbc1633b /kernel/declarations.ml | |
| parent | 78e28c6538b5daf26d84e3acd2c611a838ceeda3 (diff) | |
| parent | d5b15b97afbdb324d708d24cb1032a1a15d0c680 (diff) | |
Merge PR #11240: Add rew dependent Notations
Reviewed-by: herbelin
Ack-by: jfehrle
Diffstat (limited to 'kernel/declarations.ml')
0 files changed, 0 insertions, 0 deletions