diff options
Diffstat (limited to 'pretyping/coercion.ml')
| -rw-r--r-- | pretyping/coercion.ml | 28 |
1 files changed, 16 insertions, 12 deletions
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index 8ebb8cd2..e61e52c1 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -295,8 +295,8 @@ and coerce loc env evdref (x : Term.constr) (y : Term.constr) let evm = !evdref in (try subco () with NoSubtacCoercion -> - let typ = Typing.type_of env evm c in - let typ' = Typing.type_of env evm c' in + let typ = Typing.unsafe_type_of env evm c in + let typ' = Typing.unsafe_type_of env evm c' in (* if not (is_arity env evm typ) then *) coerce_application typ typ' c c' l l') (* else subco () *) @@ -305,8 +305,8 @@ and coerce loc env evdref (x : Term.constr) (y : Term.constr) | x, y when Constr.equal c c' -> if Int.equal (Array.length l) (Array.length l') then let evm = !evdref in - let lam_type = Typing.type_of env evm c in - let lam_type' = Typing.type_of env evm c' in + let lam_type = Typing.unsafe_type_of env evm c in + let lam_type' = Typing.unsafe_type_of env evm c' in (* if not (is_arity env evm lam_type) then ( *) coerce_application lam_type lam_type' c c' l l' (* ) else subco () *) @@ -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) @@ -378,7 +379,8 @@ let inh_app_fun env evd j = try let t,p = lookup_path_to_fun_from env evd j.uj_type in apply_coercion env evd p j t - with Not_found | NoCoercion when Flags.is_program_mode () -> + with Not_found | NoCoercion -> + if Flags.is_program_mode () then try let evdref = ref evd in let coercef, t = mu env evdref t in @@ -386,15 +388,17 @@ let inh_app_fun env evd j = (!evdref, res) with NoSubtacCoercion | NoCoercion -> (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 |