diff options
| author | Pierre Boutillier | 2014-04-10 15:59:45 +0200 |
|---|---|---|
| committer | Pierre Boutillier | 2014-04-10 16:25:08 +0200 |
| commit | 29de26213adaa8b75320bee6897218d5e8d54663 (patch) | |
| tree | 85b703db6834ee0e086c81143f2463527653c354 /kernel/inductive.ml | |
| parent | 6e66d8c551b5edcb33a9f3fbf744b2f82d944c50 (diff) | |
By resolution of the CoqWG, instantiate must not be used now that refine works
Diffstat (limited to 'kernel/inductive.ml')
0 files changed, 0 insertions, 0 deletions