1 files changed, 75 insertions, 45 deletions

diff --git a/tactics/hints.ml b/tactics/hints.ml
index 41b200bb83..4532f97a27 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -42,21 +42,22 @@ type debug = Debug | Info | Off
 
 exception Bound
 
-let head_constr_bound sigma t =
-  let t = strip_outer_cast sigma t in
-  let _,ccl = decompose_prod_assum sigma t in
-  let hd,args = decompose_app sigma ccl in
-  let open GlobRef in
-  match EConstr.kind sigma hd with
-  | Const (c, _) -> ConstRef c
-  | Ind (i, _) -> IndRef i
-  | Construct (c, _) -> ConstructRef c
-  | Var id -> VarRef id
-  | Proj (p, _) -> ConstRef (Projection.constant p)
-  | _ -> raise Bound
+let rec head_bound sigma t = match EConstr.kind sigma t with
+| Prod (_, _, b)  -> head_bound sigma b
+| LetIn (_, _, _, b) -> head_bound sigma b
+| App (c, _) -> head_bound sigma c
+| Case (_, _, _, c, _) -> head_bound sigma c
+| Ind (ind, _) -> GlobRef.IndRef ind
+| Const (c, _) -> GlobRef.ConstRef c
+| Construct (c, _) -> GlobRef.ConstructRef c
+| Var id -> GlobRef.VarRef id
+| Proj (p, _) -> GlobRef.ConstRef (Projection.constant p)
+| Cast (c, _, _) -> head_bound sigma c
+| Evar _ | Rel _ | Meta _ | Sort _ | Fix _ | Lambda _
+| CoFix _ | Int _ | Float _ | Array _ -> raise Bound
 
 let head_constr sigma c =
-  try head_constr_bound sigma c
+  try head_bound sigma c
   with Bound -> user_err (Pp.str "Head identifier must be a constant, section variable, \
                                   (co)inductive type, (co)inductive type constructor, or projection.")
 
@@ -105,7 +106,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 =
@@ -237,10 +238,38 @@ let pri_order t1 t2 = pri_order_int t1 t2 <= 0
 type stored_data = int * full_hint
     (* First component is the index of insertion in the table, to keep most recent first semantics. *)
 
-module Bounded_net = Btermdn.Make(struct
-                                    type t = stored_data
-                                    let compare = pri_order_int
-                                  end)
+module Bounded_net :
+sig
+  type t
+  val empty : t
+  val add : TransparentState.t option -> t -> Pattern.constr_pattern -> stored_data -> t
+  val lookup : Evd.evar_map -> TransparentState.t option -> t -> EConstr.constr -> stored_data list
+end =
+struct
+  module Data = struct type t = stored_data let compare = pri_order_int end
+  module Bnet = Btermdn.Make(Data)
+
+  type diff = TransparentState.t option * Pattern.constr_pattern * stored_data
+  type data = Bnet of Bnet.t | Diff of diff * data ref
+  type t = data ref
+
+  let empty = ref (Bnet Bnet.empty)
+
+  let add st net p v = ref (Diff ((st, p, v), net))
+
+  let rec force net = match !net with
+  | Bnet dn -> dn
+  | Diff ((st, p, v), rem) ->
+    let dn = force rem in
+    let p = Bnet.pattern st p in
+    let dn = Bnet.add dn p v in
+    let () = net := (Bnet dn) in
+    dn
+
+  let lookup sigma st net p =
+    let dn = force net in
+    Bnet.lookup sigma st dn p
+end
 
 type search_entry = {
   sentry_nopat : stored_data list;
@@ -263,18 +292,17 @@ let add_tac pat t se =
   | None ->
     if List.exists (eq_pri_auto_tactic t) se.sentry_nopat then se
     else { se with sentry_nopat = List.insert pri_order t se.sentry_nopat }
-  | Some pat ->
+  | Some (st, pat) ->
     if List.exists (eq_pri_auto_tactic t) se.sentry_pat then se
     else { se with
         sentry_pat = List.insert pri_order t se.sentry_pat;
-        sentry_bnet = Bounded_net.add se.sentry_bnet pat t; }
+        sentry_bnet = Bounded_net.add st se.sentry_bnet pat t; }
 
 let rebuild_dn st se =
   let dn' =
     List.fold_left
       (fun dn (id, t) ->
-        let pat = Bounded_net.pattern (Some st) (Option.get t.pat) in
-        Bounded_net.add dn pat (id, t))
+        Bounded_net.add (Some st) dn (Option.get t.pat) (id, t))
       Bounded_net.empty se.sentry_pat
   in
   { se with sentry_bnet = dn' }
@@ -322,8 +350,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 } }
 
@@ -650,7 +677,7 @@ struct
           if not db.use_dn && is_exact v.code.obj then None
           else
             let dnst = if db.use_dn then Some db.hintdb_state else None in
-            Option.map (fun p -> Bounded_net.pattern dnst p) v.pat
+            Option.map (fun p -> (dnst, p)) v.pat
         in
           let oval = find gr db in
             { db with hintdb_map = GlobRef.Map.add gr (add_tac pat idv oval) db.hintdb_map }
@@ -775,12 +802,6 @@ let rec nb_hyp sigma c = match EConstr.kind sigma c with
 
 (* adding and removing tactics in the search table *)
 
-let try_head_pattern c =
-  try head_pattern_bound c
-  with BoundPattern ->
-    user_err (Pp.str "Head pattern or sub-pattern must be a global constant, a section variable, \
-                      an if, case, or let expression, an application, or a projection.")
-
 let with_uid c = { obj = c; uid = fresh_key () }
 
 let secvars_of_idset s =
@@ -801,15 +822,15 @@ let make_exact_entry env sigma info ~poly ?(name=PathAny) (c, cty, ctx) =
     match EConstr.kind sigma cty with
     | Prod _ -> failwith "make_exact_entry"
     | _ ->
-        let pat = Patternops.pattern_of_constr env sigma (EConstr.to_constr ~abort_on_undefined_evars:false sigma cty) in
         let hd =
-          try head_pattern_bound pat
-          with BoundPattern -> failwith "make_exact_entry"
+          try head_bound sigma cty
+          with Bound -> failwith "make_exact_entry"
         in
         let pri = match info.hint_priority with None -> 0 | Some p -> p in
         let pat = match info.hint_pattern with
         | Some pat -> snd pat
-        | None -> pat
+        | None ->
+          Patternops.pattern_of_constr env sigma (EConstr.to_constr ~abort_on_undefined_evars:false sigma cty)
         in
         (Some hd,
          { pri; pat = Some pat; name;
@@ -823,16 +844,17 @@ let make_apply_entry env sigma (eapply,hnf,verbose) info ~poly ?(name=PathAny) (
     let sigma' = Evd.merge_context_set univ_flexible sigma ctx in
     let ce = mk_clenv_from_env env sigma' None (c,cty) in
     let c' = clenv_type (* ~reduce:false *) ce in
-    let pat = Patternops.pattern_of_constr env ce.evd (EConstr.to_constr ~abort_on_undefined_evars:false sigma c') in
     let hd =
-      try head_pattern_bound pat
-      with BoundPattern -> failwith "make_apply_entry" in
+      try head_bound ce.evd c'
+      with Bound -> failwith "make_apply_entry" in
     let miss = clenv_missing ce in
     let nmiss = List.length miss in
     let secvars = secvars_of_constr env sigma c in
     let pri = match info.hint_priority with None -> nb_hyp sigma' cty + nmiss | Some p -> p in
     let pat = match info.hint_pattern with
-      | Some p -> snd p | None -> pat
+    | Some p -> snd p
+    | None ->
+      Patternops.pattern_of_constr env ce.evd (EConstr.to_constr ~abort_on_undefined_evars:false sigma c')
     in
     if Int.equal nmiss 0 then
       (Some hd,
@@ -935,14 +957,21 @@ let make_unfold eref =
      code = with_uid (Unfold_nth eref) })
 
 let make_extern pri pat tacast =
-  let hdconstr = Option.map try_head_pattern pat in
+  let hdconstr = match pat with
+  | None -> None
+  | Some c ->
+    try Some (head_pattern_bound c)
+    with BoundPattern ->
+      user_err (Pp.str "Head pattern or sub-pattern must be a global constant, a section variable, \
+                        an if, case, or let expression, an application, or a projection.")
+  in
   (hdconstr,
    { pri = pri;
      pat = pat;
      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
@@ -1076,7 +1105,7 @@ let subst_autohint (subst, obj) =
     match t with
     | None -> gr'
     | Some t ->
-      (try head_constr_bound Evd.empty (EConstr.of_constr t.Univ.univ_abstracted_value)
+      (try head_bound Evd.empty (EConstr.of_constr t.Univ.univ_abstracted_value)
        with Bound -> gr')
   in
   let subst_mps subst c = EConstr.of_constr (subst_mps subst (EConstr.Unsafe.to_constr c)) in
@@ -1106,9 +1135,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
@@ -1388,7 +1418,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) =