diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-07-10 01:17:56 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-07-10 19:18:41 +0200 |
| commit | 2aaced1d2486deb901ea0a5b134ef28273dda67f (patch) | |
| tree | d5d7cccb1fc0b6d9132e1f5fcdc0d1a8b3afb7ff /pretyping/coercion.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 'pretyping/coercion.ml')
| -rw-r--r-- | pretyping/coercion.ml | 18 |
1 files changed, 10 insertions, 8 deletions
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index 6765ca130..e61e52c17 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -345,7 +345,7 @@ let saturate_evd env evd = Typeclasses.resolve_typeclasses ~filter:Typeclasses.no_goals ~split:false ~fail:false env evd -(* appliquer le chemin de coercions p à hj *) +(* Apply coercion path from p to hj; raise NoCoercion if not applicable *) let apply_coercion env sigma p hj typ_cl = try let j,t,evd = @@ -367,7 +367,8 @@ let apply_coercion env sigma p hj typ_cl = with NoCoercion as e -> raise e | e when Errors.noncritical e -> anomaly (Pp.str "apply_coercion") -let inh_app_fun env evd j = +(* Try to coerce to a funclass; raise NoCoercion if not possible *) +let inh_app_fun_core env evd j = let t = whd_betadeltaiota env evd j.uj_type in match kind_of_term t with | Prod (_,_,_) -> (evd,j) @@ -387,16 +388,17 @@ let inh_app_fun env evd j = (!evdref, res) with NoSubtacCoercion | NoCoercion -> (evd,j) - else (evd, j) + else raise NoCoercion +(* Try to coerce to a funclass; returns [j] if no coercion is applicable *) let inh_app_fun resolve_tc env evd j = - try inh_app_fun env evd j + try inh_app_fun_core env evd j with - | Not_found when not resolve_tc + | NoCoercion when not resolve_tc || not !use_typeclasses_for_conversion -> (evd, j) - | Not_found -> - try inh_app_fun env (saturate_evd env evd) j - with Not_found -> (evd, j) + | NoCoercion -> + try inh_app_fun_core env (saturate_evd env evd) j + with NoCoercion -> (evd, j) let inh_tosort_force loc env evd j = try |