diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-03-07 20:55:31 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-03-07 20:55:31 +0000 |
| commit | 8e4b7319caa0754401c8b868e9ce9490a867d7f1 (patch) | |
| tree | efbb3e085ff7f28dc8310bc906189846f69cf32d /pretyping/coercion.ml | |
| parent | a5808860fbabd1239d1116c2f4413d56ff99620f (diff) | |
Reverted commit r13893 about propagation of more informative
unification failure messages (it is not fully usable and was not
intended to be committed now, sorry for the noise).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13895 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/coercion.ml')
| -rw-r--r-- | pretyping/coercion.ml | 13 |
1 files changed, 6 insertions, 7 deletions
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index bedd3eb74..5503a147a 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -79,7 +79,6 @@ end module Default = struct (* Typing operations dealing with coercions *) exception NoCoercion - exception NoCoercionNoUnifier of evar_map * unification_error (* Here, funj is a coercion therefore already typed in global context *) let apply_coercion_args env argl funj = @@ -187,11 +186,11 @@ module Default = struct with Not_found -> raise NoCoercion in try (the_conv_x_leq env t' c1 evd, v') - with NotUnifiable _ -> raise NoCoercion + with Reduction.NotConvertible -> raise NoCoercion let rec inh_conv_coerce_to_fail loc env evd rigidonly v t c1 = try (the_conv_x_leq env t c1 evd, v) - with NotUnifiable (best_failed_evd,e) -> + with Reduction.NotConvertible -> try inh_coerce_to_fail env evd rigidonly v t c1 with NoCoercion -> match @@ -219,7 +218,7 @@ module Default = struct | Some v2 -> Retyping.get_type_of env1 evd' v2 in let (evd'',v2') = inh_conv_coerce_to_fail loc env1 evd' rigidonly v2 t2 u2 in (evd'', Option.map (fun v2' -> mkLambda (name, u1, v2')) v2') - | _ -> raise (NoCoercionNoUnifier (best_failed_evd,e)) + | _ -> raise NoCoercion (* Look for cj' obtained from cj by inserting coercions, s.t. cj'.typ = t *) let inh_conv_coerce_to_gen rigidonly loc env evd cj (n, t) = @@ -228,12 +227,12 @@ module Default = struct let (evd', val') = try inh_conv_coerce_to_fail loc env evd rigidonly (Some cj.uj_val) cj.uj_type t - with NoCoercionNoUnifier (best_failed_evd,e) -> + with NoCoercion -> let evd = saturate_evd env evd in try inh_conv_coerce_to_fail loc env evd rigidonly (Some cj.uj_val) cj.uj_type t - with NoCoercionNoUnifier _ -> - error_actual_type_loc loc env best_failed_evd cj t e + with NoCoercion -> + error_actual_type_loc loc env evd cj t in let val' = match val' with Some v -> v | None -> assert(false) in (evd',{ uj_val = val'; uj_type = t }) |