diff options
| author | Pierre-Marie Pédrot | 2018-10-19 15:27:55 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-10-19 15:27:55 +0200 |
| commit | 3799939088b5aa616974a0d37de7e2616024f222 (patch) | |
| tree | 808e60e5546489a694e1da784bd4895bc0195172 /kernel/nativecode.ml | |
| parent | 6ab9a8088394b710ae0b9f6d5711d2fe0509419f (diff) | |
| parent | e050884da17b260934a428d5b1bb11cd788ae0e1 (diff) | |
Merge PR #8724: [universes] deprecate constr_of_global
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions