From 21b4e41544f03de18d9f5b1bdb93a26b36a97999 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 8 Jun 2020 15:17:33 +0200
Subject: Opacify the type of hint metadata.

---
 plugins/firstorder/sequent.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins')

diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml
index 3dd5059e5d..e365151079 100644
--- a/plugins/firstorder/sequent.ml
+++ b/plugins/firstorder/sequent.ml
@@ -205,7 +205,7 @@ open Hints
 
 let extend_with_auto_hints env sigma l seq =
   let f (seq,sigma) p_a_t =
-    match repr_hint p_a_t.code with
+    match FullHint.repr p_a_t with
     | Res_pf (c,_) | Give_exact (c,_)
     | Res_pf_THEN_trivial_fail (c,_) ->
       let (c, _, _) = c in
-- 
cgit v1.2.3