From 85f1d9ca4b10a80be6929c81e2e6ca4c7634f619 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Wed, 12 Feb 2014 10:27:32 +0100
Subject: TC: honor the use_typeclasses flag in pretyping

The coercion code was not seeing such flag and always trying
to resolve type classes.  In particular open_contr is pretyped
without type classes.
---
 proofs/goal.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'proofs')

diff --git a/proofs/goal.ml b/proofs/goal.ml
index c40570c2c5..4d1aa41248 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -193,7 +193,7 @@ module Refinable = struct
     let my_type = Retyping.get_type_of env !rdefs t in
     let j = Environ.make_judge t my_type in
     let (new_defs,j') =
-      Coercion.inh_conv_coerce_to (Loc.ghost) env !rdefs j typ
+      Coercion.inh_conv_coerce_to true (Loc.ghost) env !rdefs j typ
     in
     rdefs := new_defs;
     j'.Environ.uj_val
-- 
cgit v1.2.3