From e9bbfcd6d589a9e8e5abcd9fbc852a77996c97db Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Tue, 13 Nov 2018 10:11:15 +0100
Subject: Declare initial hint databases in prelude

Previously, they were hard-wired in the ML code.
---
 pretyping/pretyping.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 8e9a2e114b..fa64c21d1e 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -265,8 +265,8 @@ let apply_inference_hook hook env sigma frozen = match frozen with
 
 let apply_heuristics env sigma fail_evar =
   (* Resolve eagerly, potentially making wrong choices *)
-  try solve_unif_constraints_with_heuristics
-        ~flags:(default_flags_of (Typeclasses.classes_transparent_state ())) env sigma
+  let flags = default_flags_of (Typeclasses.classes_transparent_state ()) in
+  try solve_unif_constraints_with_heuristics ~flags env sigma
   with e when CErrors.noncritical e ->
     let e = CErrors.push e in
     if fail_evar then iraise e else sigma
-- 
cgit v1.2.3