diff options
| author | Gaëtan Gilbert | 2019-11-01 19:38:01 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-11-01 19:38:01 +0100 |
| commit | 66c7622ba84284135dc821ab5eee7f79102e0c59 (patch) | |
| tree | 502fafffb6727c2bc774e5aaa4f4db6a1a43e23d /kernel/nativelambda.mli | |
| parent | 1e0e9dc1d9afdec7b33b72178487ede494520e06 (diff) | |
| parent | c0f7d897fc6d831de44211f75945f51603a0c6ed (diff) | |
Merge PR #10647: Expose universe processing in comInductive.
Reviewed-by: SkySkimmer
Reviewed-by: ppedrot
Diffstat (limited to 'kernel/nativelambda.mli')
0 files changed, 0 insertions, 0 deletions