Ensure statically that Hint Extern comes with a pattern.

5 files changed, 11 insertions, 12 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 0931c3e61e..488bcb5208 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -369,8 +369,7 @@ and tac_of_hint dbg db_list local_db concl (flags, h) =
          let info = Exninfo.reify () in
          Tacticals.New.tclFAIL ~info 0 (str"Unbound reference")
        end
-    | Extern tacast ->
-      let p = FullHint.pattern h in
+    | Extern (p, tacast) ->
       conclPattern concl p tacast
   in
   let pr_hint env sigma =
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 36544883aa..378a3e718b 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -359,7 +359,7 @@ and e_my_find_search db_list local_db secvars hdc complete only_classes env sigm
          Tacticals.New.tclTHEN fst snd
       | Unfold_nth c ->
          Proofview.tclPROGRESS (unfold_in_concl [AllOccurrences,c])
-      | Extern tacast -> conclPattern concl p tacast
+      | Extern (p, tacast) -> conclPattern concl p tacast
       in
       let tac = FullHint.run h tac in
       let tac = if complete then Tacticals.New.tclCOMPLETE tac else tac in
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index 9a554b117e..17e6a6edb4 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -126,7 +126,7 @@ and e_my_find_search env sigma db_list local_db secvars concl =
         Tacticals.New.tclTHEN (unify_e_resolve st h)
           (e_trivial_fail_db db_list local_db)
       | Unfold_nth c -> reduce (Unfold [AllOccurrences,c]) onConcl
-      | Extern tacast -> conclPattern concl (FullHint.pattern h) tacast
+      | Extern (pat, tacast) -> conclPattern concl pat tacast
       in
       let tac = FullHint.run h tac in
       (tac, b, lazy (FullHint.print env sigma h))
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 0ab1adda4b..0b11c1e79f 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -105,7 +105,7 @@ type 'a hint_ast =
   | Give_exact of 'a
   | Res_pf_THEN_trivial_fail of 'a (* Hint Immediate *)
   | Unfold_nth of evaluable_global_reference       (* Hint Unfold *)
-  | Extern     of Genarg.glob_generic_argument (* Hint Extern *)
+  | Extern     of Pattern.constr_pattern option * Genarg.glob_generic_argument (* Hint Extern *)
 
 
 type 'a hints_path_atom_gen =
@@ -349,8 +349,7 @@ let instantiate_hint env sigma p =
     | Res_pf_THEN_trivial_fail c ->
       Res_pf_THEN_trivial_fail (mk_clenv c)
     | Give_exact c -> Give_exact (mk_clenv c)
-    | Unfold_nth e -> Unfold_nth e
-    | Extern t -> Extern t
+    | (Unfold_nth _ | Extern _) as h -> h
   in
   { p with code = { p.code with obj = code } }
 
@@ -969,7 +968,7 @@ let make_extern pri pat tacast =
      name = PathAny;
      db = None;
      secvars = Id.Pred.empty; (* Approximation *)
-     code = with_uid (Extern tacast) })
+     code = with_uid (Extern (pat, tacast)) })
 
 let make_mode ref m =
   let open Term in
@@ -1133,9 +1132,10 @@ let subst_autohint (subst, obj) =
       | Unfold_nth ref ->
           let ref' = subst_evaluable_reference subst ref in
           if ref==ref' then data.code.obj else Unfold_nth ref'
-      | Extern tac ->
+      | Extern (pat, tac) ->
+          let pat' = Option.Smart.map (subst_pattern env sigma subst) data.pat in
           let tac' = Genintern.generic_substitute subst tac in
-          if tac==tac' then data.code.obj else Extern tac'
+          if pat==pat' && tac==tac' then data.code.obj else Extern (pat', tac')
     in
     let name' = subst_path_atom subst data.name in
     let uid' = subst_kn subst data.code.uid in
@@ -1415,7 +1415,7 @@ let pr_hint env sigma h = match h.obj with
       (str"simple apply " ++ pr_hint_elt env sigma c ++ str" ; trivial")
   | Unfold_nth c ->
     str"unfold " ++  pr_evaluable_reference c
-  | Extern tac ->
+  | Extern (_, tac) ->
     str "(*external*) " ++ Pputils.pr_glb_generic env sigma tac
 
 let pr_id_hint env sigma (id, v) =
diff --git a/tactics/hints.mli b/tactics/hints.mli
index f0fed75828..0b9da27ab3 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -37,7 +37,7 @@ type 'a hint_ast =
   | Give_exact of 'a
   | Res_pf_THEN_trivial_fail of 'a (* Hint Immediate *)
   | Unfold_nth of evaluable_global_reference       (* Hint Unfold *)
-  | Extern     of Genarg.glob_generic_argument       (* Hint Extern *)
+  | Extern     of Pattern.constr_pattern option * Genarg.glob_generic_argument       (* Hint Extern *)
 
 type hint = private {
   hint_term : constr;