diff options
| author | Pierre-Marie Pédrot | 2015-06-01 11:40:35 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-06-01 11:40:35 +0200 |
| commit | dc2405f017f5b784d3c7393ae2b4ba1ef710d10b (patch) | |
| tree | ea2defb1691834c73f35bb9cf8912cdb04f3f7b8 /pretyping | |
| parent | 3fcadca93b8d9dd70d9d93412cbacf8d4e851ed7 (diff) | |
| parent | 43aa642ad4f2d30029c1c1f272ba162b6801a40b (diff) | |
Merge branch 'v8.5'
Diffstat (limited to 'pretyping')
| -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 f5135f5c60..6765ca130b 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 |