diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-05-15 14:26:35 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-05-15 14:26:35 +0200 |
| commit | 4944b5e72c0f4bfcf1ae140f810d8666dac3cf60 (patch) | |
| tree | 150ca7467f78254505edf46edf33247fade17170 /pretyping/coercion.ml | |
| parent | 3fb81febe8efc34860688cac88a2267cfe298cf7 (diff) | |
Make Coercion.inh_app_fun respect its specification.
It enhances bug #3527, as instead of raising an anomaly "Uncaught
exception Coercion.NoCoercion(_)", it now fails with a typing error.
Diffstat (limited to 'pretyping/coercion.ml')
| -rw-r--r-- | pretyping/coercion.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index f5135f5c6..6765ca130 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -378,7 +378,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,6 +387,7 @@ let inh_app_fun env evd j = (!evdref, res) with NoSubtacCoercion | NoCoercion -> (evd,j) + else (evd, j) let inh_app_fun resolve_tc env evd j = try inh_app_fun env evd j |