diff options
| author | Matthieu Sozeau | 2014-06-26 14:11:05 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-06-26 14:11:05 +0200 |
| commit | dd33100f78b738e0268e3a65040a1b3ee9b3facf (patch) | |
| tree | 97dd1f47a9bf2e3182a476750fccc8b26af45053 /pretyping | |
| parent | 4cd36df8879ae02639b3c8cf3712df6296e68a4c (diff) | |
Add an option to disable typeclass resolution during conversion, which
is has non-local effects. For now it is not disabled by default, but we'll
try to disable it once the test-suite and contribs are stabilized.
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/coercion.ml | 17 |
1 files changed, 15 insertions, 2 deletions
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index 125517aec5..dfaff327ab 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -30,6 +30,18 @@ open Evd open Termops open Globnames +let use_typeclasses_for_conversion = ref true + +let _ = + Goptions.declare_bool_option + { Goptions.optsync = true; + optdepr = false; + optname = "use typeclass resolution during conversion"; + optkey = ["Typeclass"; "Resolution"; "For"; "Conversion"]; + optread = (fun () -> !use_typeclasses_for_conversion); + optwrite = (fun b -> use_typeclasses_for_conversion := b) } + + (* Typing operations dealing with coercions *) exception NoCoercion exception NoCoercionNoUnifier of evar_map * unification_error @@ -371,7 +383,8 @@ let inh_app_fun env evd j = let inh_app_fun resolve_tc env evd j = try inh_app_fun env evd j with - | Not_found when not resolve_tc -> (evd, j) + | Not_found when not resolve_tc + || not !use_typeclasses_for_conversion -> (evd, j) | Not_found -> try inh_app_fun env (saturate_evd env evd) j with Not_found -> (evd, j) @@ -475,7 +488,7 @@ let inh_conv_coerce_to_gen resolve_tc rigidonly loc env evd cj t = coerce_itf loc env evd (Some cj.uj_val) cj.uj_type t else raise NoSubtacCoercion with - | NoSubtacCoercion when not resolve_tc -> + | NoSubtacCoercion when not resolve_tc || not !use_typeclasses_for_conversion -> error_actual_type_loc loc env best_failed_evd cj t e | NoSubtacCoercion -> let evd' = saturate_evd env evd in |