diff options
| author | msozeau | 2012-07-11 16:03:41 +0000 |
|---|---|---|
| committer | msozeau | 2012-07-11 16:03:41 +0000 |
| commit | e6bf1b6936f8bd61eb1266f7f4dd67181f3630f1 (patch) | |
| tree | 1d23e04205c4ceaadd6c6c68ac95d7a9287609df | |
| parent | f13b87b5b1a2f5d35b1be51d25d0891a2db08b95 (diff) | |
Fix regression introduced in r15418 that broke MathClasses. In program mode, try program coercions before
the last resort typeclass resolution to resolve a conversion problem.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15595 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | pretyping/coercion.ml | 24 |
1 files changed, 11 insertions, 13 deletions
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index 524d9d058e..7fd4d1cc29 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -319,11 +319,9 @@ let coerce_itf loc env isevars v t c1 = let t = Option.map (app_opt env evars coercion) v in !evars, t - - let saturate_evd env evd = Typeclasses.resolve_typeclasses - ~filter:Typeclasses.no_goals ~split:true ~fail:false env evd + ~filter:Typeclasses.no_goals ~split:false ~fail:false env evd (* appliquer le chemin de coercions p à hj *) let apply_coercion env sigma p hj typ_cl = @@ -461,16 +459,16 @@ let inh_conv_coerce_to_gen rigidonly loc env evd cj t = try inh_conv_coerce_to_fail loc env evd rigidonly (Some cj.uj_val) cj.uj_type t 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 NoCoercion -> - (if Flags.is_program_mode () then - try - coerce_itf loc env evd (Some cj.uj_val) cj.uj_type t - with NoSubtacCoercion -> - error_actual_type_loc loc env evd cj t - else error_actual_type_loc loc env evd cj t) + try + if Flags.is_program_mode () then + coerce_itf loc env evd (Some cj.uj_val) cj.uj_type t + else raise NoSubtacCoercion + with NoSubtacCoercion -> + 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 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 }) |