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


From 9eca7cca68dc82aa738a8d408d75e1b9b5405646 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 8 Jun 2020 18:57:25 +0200
Subject: Wrap the content of full hints into a record.

---
 plugins/firstorder/sequent.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'plugins')

diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml
index e365151079..db3631daa4 100644
--- a/plugins/firstorder/sequent.ml
+++ b/plugins/firstorder/sequent.ml
@@ -206,9 +206,9 @@ open Hints
 let extend_with_auto_hints env sigma l seq =
   let f (seq,sigma) p_a_t =
     match FullHint.repr p_a_t with
-    | Res_pf (c,_) | Give_exact (c,_)
-    | Res_pf_THEN_trivial_fail (c,_) ->
-      let (c, _, _) = c in
+    | Res_pf c | Give_exact c
+    | Res_pf_THEN_trivial_fail c ->
+      let c = c.hint_term in
       (match  EConstr.destRef sigma c with
        | exception Constr.DestKO -> seq, sigma
        | gr, _ ->
-- 
cgit v1.2.3