Exporting the original unprocessed hint in the hint running function.

7 files changed, 28 insertions, 17 deletions

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
diff --git a/tactics/auto.ml b/tactics/auto.ml
index e5fdf6a7c..72c28ce32 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -93,6 +93,7 @@ let unify_resolve_gen poly = function
   | Some flags -> unify_resolve poly flags
 
 let exact poly (c,clenv) =
+  let (c, _, _) = c in
   let ctx, c' = 
     if poly then
       let evd', subst = Evd.refresh_undefined_universes clenv.evd in
diff --git a/tactics/auto.mli b/tactics/auto.mli
index 8dacc1362..6e2acf7f5 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -26,9 +26,9 @@ val default_search_depth : int ref
 val auto_flags_of_state : transparent_state -> Unification.unify_flags
 
 (** Try unification with the precompiled clause, then use registered Apply *)
-val unify_resolve_nodelta : polymorphic -> (constr * clausenv) -> unit Proofview.tactic
+val unify_resolve_nodelta : polymorphic -> (raw_hint * clausenv) -> unit Proofview.tactic
 
-val unify_resolve : polymorphic -> Unification.unify_flags -> (constr * clausenv) -> unit Proofview.tactic
+val unify_resolve : polymorphic -> Unification.unify_flags -> (raw_hint * clausenv) -> unit Proofview.tactic
 
 (** [ConclPattern concl pat tacast]:
    if the term concl matches the pattern pat, (in sense of
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index ed5b783f6..36b60385d 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -141,6 +141,7 @@ let progress_evars t =
 
 
 let e_give_exact flags poly (c,clenv) gl =
+  let (c, _, _) = c in
   let c, gl =
     if poly then
       let clenv', subst = Clenv.refresh_undefined_univs clenv in
@@ -166,6 +167,7 @@ let unify_resolve poly flags (c,clenv) gls =
     (Clenvtac.clenv_refine false ~with_classes:false clenv') gls
 
 let clenv_of_prods poly nprods (c, clenv) gls =
+  let (c, _, _) = c in
   if poly || Int.equal nprods 0 then Some clenv
   else
     let ty = pf_unsafe_type_of gls c in
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index b6b18719c..09c5fa873 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -118,6 +118,7 @@ open Unification
 let priority l = List.map snd (List.filter (fun (pr,_) -> Int.equal pr 0) l)
 
 let unify_e_resolve poly flags (c,clenv) gls =
+  let (c, _, _) = c in
   let clenv', subst = if poly then Clenv.refresh_undefined_univs clenv 
   else clenv, Univ.empty_level_subst in
   let clenv' = connect_clenv gls clenv' in
@@ -134,6 +135,7 @@ let hintmap_of hdc concl =
    (* FIXME: should be (Hint_db.map_eauto hdc concl db) *)
 
 let e_exact poly flags (c,clenv) =
+  let (c, _, _) = c in
   let clenv', subst = 
     if poly then Clenv.refresh_undefined_univs clenv 
     else clenv, Univ.empty_level_subst
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 9faa96a80..96c7d79ca 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -97,7 +97,9 @@ type 'a with_uid = {
   uid : KerName.t;
 }
 
-type hint = (constr * clausenv) hint_ast with_uid
+type raw_hint = constr * types * Univ.universe_context_set
+
+type hint = (raw_hint * clausenv) hint_ast with_uid
 
 type 'a with_metadata = {
   pri  : int;            (* A number lower is higher priority *)
@@ -110,7 +112,7 @@ type 'a with_metadata = {
 type full_hint = hint with_metadata
 
 type hint_entry = global_reference option * 
-  (constr * types * Univ.universe_context_set) hint_ast with_uid with_metadata
+  raw_hint hint_ast with_uid with_metadata
 
 type import_level = [ `LAX | `WARN | `STRICT ]
 
@@ -267,7 +269,7 @@ let strip_params env c =
   | _ -> c
 
 let instantiate_hint env sigma p =
-  let mk_clenv c cty ctx =
+  let mk_clenv (c, cty, ctx) =
     let sigma = Evd.merge_context_set univ_flexible sigma ctx in
     let cl = mk_clenv_from_env env sigma None (c,cty) in 
       {cl with templval = 
@@ -275,11 +277,11 @@ let instantiate_hint env sigma p =
 	env = empty_env}
   in
   let code = match p.code.obj with
-    | Res_pf (c, cty, ctx) -> Res_pf (c, mk_clenv c cty ctx)
-    | ERes_pf (c, cty, ctx) -> ERes_pf (c, mk_clenv c cty ctx)
-    | Res_pf_THEN_trivial_fail (c, cty, ctx) ->
-      Res_pf_THEN_trivial_fail (c, mk_clenv c cty ctx)
-    | Give_exact (c, cty, ctx) -> Give_exact (c, mk_clenv c cty ctx)
+    | Res_pf c -> Res_pf (c, mk_clenv c)
+    | ERes_pf c -> ERes_pf (c, mk_clenv c)
+    | Res_pf_THEN_trivial_fail c ->
+      Res_pf_THEN_trivial_fail (c, mk_clenv c)
+    | Give_exact c -> Give_exact (c, mk_clenv c)
     | Unfold_nth e -> Unfold_nth e
     | Extern t -> Extern t
   in
@@ -1205,12 +1207,14 @@ let make_db_list dbnames =
 (*                    Functions for printing the hints                    *)
 (**************************************************************************)
 
+let pr_hint_elt (c, _, _) = pr_constr c
+
 let pr_hint h = match h.obj with
-  | Res_pf (c,clenv) -> (str"apply " ++ pr_constr c)
-  | ERes_pf (c,clenv) -> (str"eapply " ++ pr_constr c)
-  | Give_exact (c,clenv) -> (str"exact " ++ pr_constr c)
-  | Res_pf_THEN_trivial_fail (c,clenv) ->
-      (str"apply " ++ pr_constr c ++ str" ; trivial")
+  | Res_pf (c, _) -> (str"apply " ++ pr_hint_elt c)
+  | ERes_pf (c, _) -> (str"eapply " ++ pr_hint_elt c)
+  | Give_exact (c, _) -> (str"exact " ++ pr_hint_elt c)
+  | Res_pf_THEN_trivial_fail (c, _) ->
+      (str"apply " ++ pr_hint_elt c ++ str" ; trivial")
   | Unfold_nth c -> (str"unfold " ++  pr_evaluable_reference c)
   | Extern tac ->
       let env =
diff --git a/tactics/hints.mli b/tactics/hints.mli
index e25b66b27..af4d3d1f6 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -37,6 +37,7 @@ type 'a hint_ast =
   | Extern     of Tacexpr.glob_tactic_expr       (* Hint Extern *)
 
 type hint
+type raw_hint = constr * types * Univ.universe_context_set
 
 type hints_path_atom = 
   | PathHints of global_reference list
@@ -199,11 +200,11 @@ val make_extern :
       -> hint_entry
 
 val run_hint : hint ->
-  ((constr * clausenv) hint_ast -> 'r Proofview.tactic) -> 'r Proofview.tactic
+  ((raw_hint * clausenv) hint_ast -> 'r Proofview.tactic) -> 'r Proofview.tactic
 
 (** This function is for backward compatibility only, not to use in newly
     written code. *)
-val repr_hint : hint -> (constr * clausenv) hint_ast
+val repr_hint : hint -> (raw_hint * clausenv) hint_ast
 
 val extern_intern_tac :
   (patvar list -> Tacexpr.raw_tactic_expr -> Tacexpr.glob_tactic_expr) Hook.t