diff options
| author | Théo Zimmermann | 2019-11-25 13:27:33 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2019-11-25 13:27:33 +0100 |
| commit | 0e9cd0fe99216bc09a09a0da6906f9501b682223 (patch) | |
| tree | ee478f6fe20aed87e8239e1ee55a579eb3af528b /kernel/indTyping.ml | |
| parent | cfa4e508162e3b036e0b20e1773da4a046c274d4 (diff) | |
| parent | 461538c2fb88234c46081bc4749814ec202eaadd (diff) | |
Merge PR #11159: Minor fix in doc for [unfold]
Reviewed-by: Zimmi48
Ack-by: cpitclaudel
Diffstat (limited to 'kernel/indTyping.ml')
0 files changed, 0 insertions, 0 deletions