diff options
| author | Pierre-Marie Pédrot | 2014-12-15 07:34:22 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-12-15 07:34:22 +0100 |
| commit | 3a83f8aeeff3a4ce13c21045536e17ebb7f96677 (patch) | |
| tree | a34b8ab246bb571bf62a7a7128932c01409a31b7 /kernel/indtypes.ml | |
| parent | ab1e5d1f9180daa64924b0b398300cd311611045 (diff) | |
Fixing bug #3865.
Diffstat (limited to 'kernel/indtypes.ml')
0 files changed, 0 insertions, 0 deletions