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 /pretyping | |
| 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')
| -rw-r--r-- | pretyping/classops.mli | 4 | ||||
| -rw-r--r-- | pretyping/coercion.ml | 18 |
2 files changed, 12 insertions, 10 deletions
diff --git a/pretyping/classops.mli b/pretyping/classops.mli index c421b4505b..e2bb2d1a00 100644 --- a/pretyping/classops.mli +++ b/pretyping/classops.mli @@ -78,9 +78,9 @@ val coercion_value : coe_index -> (unsafe_judgment * bool * bool) Univ.in_univer (** {6 Lookup functions for coercion paths } *) -val lookup_path_between_class : cl_index * cl_index -> inheritance_path -(** @raise Not_found when no such path exists *) +(** @raise Not_found in the following functions when no path exists *) +val lookup_path_between_class : cl_index * cl_index -> inheritance_path val lookup_path_between : env -> evar_map -> types * types -> types * types * inheritance_path val lookup_path_to_fun_from : env -> evar_map -> types -> diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index 6765ca130b..e61e52c178 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 |