From dd33100f78b738e0268e3a65040a1b3ee9b3facf Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 26 Jun 2014 14:11:05 +0200
Subject: 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.

---
 pretyping/coercion.ml | 17 +++++++++++++++--
 1 file changed, 15 insertions(+), 2 deletions(-)

(limited to 'pretyping')

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
-- 
cgit v1.2.3