diff options
| author | Hugo Herbelin | 2015-07-10 01:17:56 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2015-07-10 19:18:41 +0200 |
| commit | 2aaced1d2486deb901ea0a5b134ef28273dda67f (patch) | |
| tree | d5d7cccb1fc0b6d9132e1f5fcdc0d1a8b3afb7ff /kernel/inductive.ml | |
| parent | 9c732a5c878bac2592cb397aca3d17cfefdcd023 (diff) | |
Continuing handling of NoCoercion after df6e64fd28 and 4944b5e72.
Commit df6e64fd28 let apply_coercion raise NoCoercion untrapped by inh_app_fun.
Commit 4944b5e72 caught NoCoercion but missed re-attempting inserting a
coercion after resolving instances of type classes.
This fixes MathClasses (while preserving fix of part of from 4944b5e72
and fixes of HoTT_coq_014.v from df6e64fd28).
Diffstat (limited to 'kernel/inductive.ml')
0 files changed, 0 insertions, 0 deletions