diff options
| author | Pierre-Marie Pédrot | 2014-04-27 21:33:58 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-04-27 21:33:58 +0200 |
| commit | 85ec7f72e1c54b5da93473f0c7a3edc8930f0d90 (patch) | |
| tree | b428162157f20d1d2d22792365400376cadc1c17 /kernel/inductive.ml | |
| parent | 7c65d85688b238a4c4197ea69df5d5af9dca7c30 (diff) | |
Giving true proof-terms in inversion instead of metas.
Diffstat (limited to 'kernel/inductive.ml')
0 files changed, 0 insertions, 0 deletions