From 36f669f769fa23eb897adfa0450875a3c0db3476 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Wed, 14 Oct 2015 12:01:38 +0200
Subject: Exporting the original unprocessed hint in the hint running function.

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

(limited to 'plugins/firstorder')

diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml
index 96c4eb01e..a77af03dc 100644
--- a/plugins/firstorder/sequent.ml
+++ b/plugins/firstorder/sequent.ml
@@ -212,6 +212,7 @@ let extend_with_auto_hints l seq gl=
     match repr_hint p_a_t.code with
 	Res_pf (c,_) | Give_exact (c,_)
       | Res_pf_THEN_trivial_fail (c,_) ->
+          let (c, _, _) = c in
 	  (try
 	     let gr = global_of_constr c in
 	     let typ=(pf_unsafe_type_of gl c) in
-- 
cgit v1.2.3