diff options
| author | Maxime Dénès | 2017-11-24 12:51:21 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2017-11-24 12:51:21 +0100 |
| commit | f9b3414888aebd1186f53c46d737536670171ab6 (patch) | |
| tree | fc0b1d05709ccbe4e3e0bf25e9a06a6b050dcae4 /kernel/constr.ml | |
| parent | 31794a1828a15acb95c235fd3166c511635add41 (diff) | |
Update PR filter used by RM.
Diffstat (limited to 'kernel/constr.ml')
0 files changed, 0 insertions, 0 deletions