diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-08-29 00:25:57 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-08-29 00:26:46 +0200 |
| commit | 23f064547758a491bb7cb709797c2b1338a17558 (patch) | |
| tree | 55523bbbca5dfb9f0090b2dce5a319c980ff178c /kernel/indtypes.mli | |
| parent | 50237af2da42eca2b1f87569433f422ae409de39 (diff) | |
Fix bug when defining primitive projections mixing defined and abstracts fields.
Diffstat (limited to 'kernel/indtypes.mli')
0 files changed, 0 insertions, 0 deletions