diff options
| author | msozeau | 2009-06-18 15:42:27 +0000 |
|---|---|---|
| committer | msozeau | 2009-06-18 15:42:27 +0000 |
| commit | 918777908845fde7b6f8e3361f2ed145eb98886b (patch) | |
| tree | 0c9652b0cd09f2bc2521878d67b4d2067c50c062 /pretyping | |
| parent | 6fd41fb09f6d809e831f2d5904f4c4b4ff2aa253 (diff) | |
Try typeclass resolution in coercion if no solution can be found to a
conversion problem. TODO: The right fix is to use constraints and
backtracking search when solving them.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12195 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/coercion.ml | 25 |
1 files changed, 18 insertions, 7 deletions
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index f8545fdc95..c0388a383a 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -101,6 +101,10 @@ module Default = struct let p = lookup_pattern_path_between (ind1,ind2) in apply_pattern_coercion loc pat p + let saturate_evd env evd = + Typeclasses.resolve_typeclasses + ~onlyargs:true ~split:true ~fail:false env evd + (* appliquer le chemin de coercions p à hj *) let apply_coercion env sigma p hj typ_cl = try @@ -125,11 +129,15 @@ module Default = struct let (evd',t) = define_evar_as_product evd ev in (evd',{ uj_val = j.uj_val; uj_type = t }) | _ -> - (try - let t,p = - lookup_path_to_fun_from env ( evd) j.uj_type in - (evd,apply_coercion env ( evd) p j t) - with Not_found -> (evd,j)) + let t,p = + lookup_path_to_fun_from env ( evd) j.uj_type in + (evd,apply_coercion env ( evd) p j t) + + let inh_app_fun env evd j = + try inh_app_fun env evd j + with Not_found -> + try inh_app_fun env (saturate_evd env evd) j + with Not_found -> (evd, j) let inh_tosort_force loc env evd j = try @@ -209,8 +217,11 @@ module Default = struct try inh_conv_coerce_to_fail loc env evd rigidonly (Some cj.uj_val) cj.uj_type t with NoCoercion -> - let sigma = evd in - error_actual_type_loc loc env sigma cj t + 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 }) |