diff options
| author | Gaëtan Gilbert | 2019-05-23 10:03:42 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-06-11 09:55:51 +0200 |
| commit | 82663b28a04d82e89bd041efd256c4838312e587 (patch) | |
| tree | 8f1c555626ebe40090143be1b663a0fe07377caf /pretyping/typeclasses_errors.ml | |
| parent | 45306c6c9c433b86406d041f58aafb7cf3a3ff82 (diff) | |
Simplify implicit_quantifiers
After removing `Instance : !type` implicit_application is only used in
constrintern. We propagate constant arguments ?allow_partial and
combine_params_freevar.
Also remove unused functions.
Diffstat (limited to 'pretyping/typeclasses_errors.ml')
0 files changed, 0 insertions, 0 deletions