Imported Upstream version 8.5~beta3+dfsg

1 files changed, 193 insertions, 99 deletions

diff --git a/tactics/hints.ml b/tactics/hints.ml
index 55d62e15..5630d20b 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -68,7 +68,7 @@ let decompose_app_bound t =
 (*           The Type of Constructions Autotactic Hints                 *)
 (************************************************************************)
 
-type 'a auto_tactic_ast =
+type 'a hint_ast =
   | Res_pf     of 'a (* Hint Apply *)
   | ERes_pf    of 'a (* Hint EApply *)
   | Give_exact of 'a
@@ -92,23 +92,66 @@ type hint_term =
   | IsGlobRef of global_reference
   | IsConstr of constr * Univ.universe_context_set
 
-type 'a auto_tactic = 'a auto_tactic_ast
+type 'a with_uid = {
+  obj : 'a;
+  uid : KerName.t;
+}
+
+type raw_hint = constr * types * Univ.universe_context_set
 
-type 'a gen_auto_tactic = {
+type hint = (raw_hint * clausenv) hint_ast with_uid
+
+type 'a with_metadata = {
   pri  : int;            (* A number lower is higher priority *)
   poly  : polymorphic;    (** Is the hint polymorpic and hence should be refreshed at each application *)
   pat  : constr_pattern option; (* A pattern for the concl of the Goal *)
   name  : hints_path_atom; (* A potential name to refer to the hint *) 
-  code : 'a     (* the tactic to apply when the concl matches pat *)
+  code : 'a;     (* the tactic to apply when the concl matches pat *)
 }
 
-type pri_auto_tactic = (constr * clausenv) auto_tactic gen_auto_tactic
+type full_hint = hint with_metadata
 
 type hint_entry = global_reference option * 
-  (constr * types * Univ.universe_context_set) auto_tactic_ast gen_auto_tactic
-
-let run_auto_tactic tac k = k tac
-let repr_auto_tactic tac = tac
+  raw_hint hint_ast with_uid with_metadata
+
+type import_level = [ `LAX | `WARN | `STRICT ]
+
+let warn_hint : import_level ref = ref `LAX
+let read_warn_hint () = match !warn_hint with
+| `LAX -> "Lax"
+| `WARN -> "Warn"
+| `STRICT -> "Strict"
+
+let write_warn_hint = function
+| "Lax" -> warn_hint := `LAX
+| "Warn" -> warn_hint := `WARN
+| "Strict" -> warn_hint := `STRICT
+| _ -> error "Only the following flags are accepted: Lax, Warn, Strict."
+
+let _ =
+  Goptions.declare_string_option
+    { Goptions.optsync  = true;
+      Goptions.optdepr  = false;
+      Goptions.optname  = "behavior of non-imported hints";
+      Goptions.optkey   = ["Loose"; "Hint"; "Behavior"];
+      Goptions.optread  = read_warn_hint;
+      Goptions.optwrite = write_warn_hint;
+    }
+
+let fresh_key =
+  let id = Summary.ref ~name:"HINT-COUNTER" 0 in
+  fun () ->
+    let cur = incr id; !id in
+    let lbl = Id.of_string ("_" ^ string_of_int cur) in
+    let kn = Lib.make_kn lbl in
+    let (mp, dir, _) = KerName.repr kn in
+    (** We embed the full path of the kernel name in the label so that the
+        identifier should be unique. This ensures that including two modules
+        together won't confuse the corresponding labels. *)
+    let lbl = Id.of_string_soft (Printf.sprintf "%s#%s#%i"
+      (ModPath.to_string mp) (DirPath.to_string dir) cur)
+    in
+    KerName.make mp dir (Label.of_id lbl)
 
 let eq_hints_path_atom p1 p2 = match p1, p2 with
 | PathHints gr1, PathHints gr2 -> List.equal eq_gr gr1 gr2
@@ -125,7 +168,7 @@ let eq_auto_tactic t1 t2 = match t1, t2 with
 | (Res_pf _ | ERes_pf _ | Give_exact _ | Res_pf_THEN_trivial_fail _
   | Unfold_nth _ | Extern _), _ -> false
 
-let eq_gen_auto_tactic t1 t2 =
+let eq_hint_metadata t1 t2 =
   Int.equal t1.pri t2.pri &&
   Option.equal constr_pattern_eq t1.pat t2.pat &&
   eq_hints_path_atom t1.name t2.name &&
@@ -153,7 +196,7 @@ let pri_order t1 t2 = pri_order_int t1 t2 <= 0
      - un discrimination net borné (Btermdn.t) constitué de tous les
        patterns de la seconde liste de tactiques *)
 
-type stored_data = int * pri_auto_tactic
+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
@@ -175,21 +218,7 @@ let empty_se = {
   sentry_mode = [];
 }
 
-let eq_pri_auto_tactic (_, x) (_, y) =
-  if Int.equal x.pri y.pri && Option.equal constr_pattern_eq x.pat y.pat then
-    match x.code,y.code with
-      | Res_pf (cstr,_),Res_pf (cstr1,_) -> 
-	  Term.eq_constr cstr cstr1
-      | ERes_pf (cstr,_),ERes_pf (cstr1,_) -> 
-	  Term.eq_constr cstr cstr1
-      | Give_exact (cstr,_),Give_exact (cstr1,_)  -> 
-	  Term.eq_constr cstr cstr1
-      | Res_pf_THEN_trivial_fail (cstr,_)
-	  ,Res_pf_THEN_trivial_fail (cstr1,_) -> 
-	  Term.eq_constr cstr cstr1
-      | _,_ -> false
-  else
-    false
+let eq_pri_auto_tactic (_, x) (_, y) = KerName.equal x.code.uid y.code.uid
 
 let add_tac pat t st se =
   match pat with
@@ -239,24 +268,24 @@ let strip_params env c =
     | _ -> c)
   | _ -> c
 
-let instantiate_hint p =
-  let mk_clenv c cty ctx =
-    let env = Global.env () in
-    let sigma = Evd.merge_context_set univ_flexible (Evd.from_env env) ctx in
-    let cl = mk_clenv_from_env (Global.env()) sigma None (c,cty) in 
+let instantiate_hint env sigma p =
+  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 = 
 	  { cl.templval with rebus = strip_params env cl.templval.rebus };
 	env = empty_env}
   in
-  let code = match p.code 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)
+  let code = match p.code.obj with
+    | 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 { pri = p.pri; poly = p.poly; name = p.name; pat = p.pat; code = code }
+  in
+  { p with code = { p.code with obj = code } }
 
 let hints_path_atom_eq h1 h2 = match h1, h2 with
 | PathHints l1, PathHints l2 -> List.equal eq_gr l1 l2
@@ -353,15 +382,19 @@ let rec normalize_path h =
 
 let path_derivate hp hint = normalize_path (path_derivate hp hint)
 
+let pp_hints_path_atom a =
+  match a with
+  | PathAny -> str"*"
+  | PathHints grs -> pr_sequence pr_global grs
+					   
 let rec pp_hints_path = function
-  | PathAtom (PathAny) -> str"."
-  | PathAtom (PathHints grs) -> pr_sequence pr_global grs
-  | PathStar p -> str "(" ++ pp_hints_path p ++ str")*"
+  | PathAtom pa -> pp_hints_path_atom pa
+  | PathStar p -> str "!(" ++ pp_hints_path p ++ str")"
   | PathSeq (p, p') -> pp_hints_path p ++ str" ; " ++ pp_hints_path p'
   | PathOr (p, p') -> 
     str "(" ++ pp_hints_path p ++ spc () ++ str"|" ++ spc () ++ pp_hints_path p' ++ str ")"
-  | PathEmpty -> str"Ø"
-  | PathEpsilon -> str"ε"
+  | PathEmpty -> str"emp"
+  | PathEpsilon -> str"eps"
 
 let subst_path_atom subst p =
   match p with
@@ -429,7 +462,9 @@ module Hint_db = struct
     else List.exists (matches_mode args) modes
 
   let merge_entry db nopat pat =
-    let h = Sort.merge pri_order (List.map snd db.hintdb_nopat @ nopat) pat in
+    let h = List.sort pri_order_int (List.map snd db.hintdb_nopat) in
+    let h = List.merge pri_order_int h nopat in
+    let h = List.merge pri_order_int h pat in
     List.map realize_tac h
 
   let map_none db =
@@ -473,15 +508,14 @@ module Hint_db = struct
     let idv = id, v in
     let k = match gr with
       | Some gr -> if db.use_dn && is_transparent_gr db.hintdb_state gr &&
-	  is_unfold v.code then None else Some gr
+	  is_unfold v.code.obj then None else Some gr
       | None -> None
     in
     let dnst = if db.use_dn then Some db.hintdb_state else None in
-    let pat = if not db.use_dn && is_exact v.code then None else v.pat in
+    let pat = if not db.use_dn && is_exact v.code.obj then None else v.pat in
       match k with
       | None ->
-          (** ppedrot: this equality here is dubious. Maybe we can remove it? *)
-          let is_present (_, (_, v')) = eq_gen_auto_tactic v v' in
+          let is_present (_, (_, v')) = KerName.equal v.code.uid v'.code.uid in
 	  if not (List.exists is_present db.hintdb_nopat) then
 	    (** FIXME *)
 	    { db with hintdb_nopat = (gr,idv) :: db.hintdb_nopat }
@@ -497,10 +531,10 @@ module Hint_db = struct
     in
       List.fold_left (fun db (gr,(id,v)) -> addkv gr id v db) db' db.hintdb_nopat
 
-  let add_one (k, v) db =
-    let v = instantiate_hint v in
+  let add_one env sigma (k, v) db =
+    let v = instantiate_hint env sigma v in
     let st',db,rebuild =
-      match v.code with
+      match v.code.obj with
       | Unfold_nth egr ->
 	  let addunf (ids,csts) (ids',csts') =
 	    match egr with
@@ -515,7 +549,7 @@ module Hint_db = struct
     let db, id = next_hint_id db in
     addkv k id v db
 
-  let add_list l db = List.fold_left (fun db k -> add_one k db) db l
+  let add_list env sigma l db = List.fold_left (fun db k -> add_one env sigma k db) db l
 
   let remove_sdl p sdl = List.smartfilter p sdl 
 
@@ -534,7 +568,9 @@ module Hint_db = struct
 
   let remove_one gr db = remove_list [gr] db
 
-  let get_entry se = List.map realize_tac (se.sentry_nopat @ se.sentry_pat)
+  let get_entry se =
+    let h = List.merge pri_order_int se.sentry_nopat se.sentry_pat in
+    List.map realize_tac h
 
   let iter f db =
     let iter_se k se = f (Some k) se.sentry_mode (get_entry se) in
@@ -586,6 +622,7 @@ let auto_init_db =
        Hintdbmap.empty)
 
 let searchtable : hint_db_table = ref auto_init_db
+let statustable = ref KNmap.empty
 
 let searchtable_map name =
   Hintdbmap.find name !searchtable
@@ -598,7 +635,7 @@ let current_pure_db () =
   List.map snd (Hintdbmap.bindings (Hintdbmap.remove "v62" !searchtable))
 
 let error_no_such_hint_database x =
-  error ("No such Hint database: "^x^".")
+  errorlabstrm "Hints" (str "No such Hint database: " ++ str x ++ str ".")
 
 (**************************************************************************)
 (*                       Definition of the summary                        *)
@@ -609,9 +646,10 @@ let add_hints_init f =
   let init = !hints_init in
   hints_init := (fun () -> init (); f ())
 
-let init     () = searchtable := auto_init_db; !hints_init ()
-let freeze   _ = !searchtable
-let unfreeze fs = searchtable := fs
+let init     () =
+  searchtable := auto_init_db; statustable := KNmap.empty; !hints_init ()
+let freeze   _ = (!searchtable, !statustable)
+let unfreeze (fs, st) = searchtable := fs; statustable := st
 
 let _ = Summary.declare_summary "search"
 	  { Summary.freeze_function   = freeze;
@@ -632,6 +670,8 @@ let try_head_pattern c =
   try head_pattern_bound c
   with BoundPattern -> error "Bound head variable."
 
+let with_uid c = { obj = c; uid = fresh_key () }
+
 let make_exact_entry env sigma pri poly ?(name=PathAny) (c, cty, ctx) =
   let cty = strip_outer_cast cty in
     match kind_of_term cty with
@@ -647,7 +687,7 @@ let make_exact_entry env sigma pri poly ?(name=PathAny) (c, cty, ctx) =
 	    poly = poly;
 	    pat = Some pat;
 	    name = name;
-	    code = Give_exact (c, cty, ctx) })
+	    code = with_uid (Give_exact (c, cty, ctx)); })
 
 let make_apply_entry env sigma (eapply,hnf,verbose) pri poly ?(name=PathAny) (c, cty, ctx) =
   let cty = if hnf then hnf_constr env sigma cty else cty in
@@ -667,7 +707,7 @@ let make_apply_entry env sigma (eapply,hnf,verbose) pri poly ?(name=PathAny) (c,
 	    poly = poly;
             pat = Some pat;
 	    name = name;
-            code = Res_pf(c,cty,ctx) })
+            code = with_uid (Res_pf(c,cty,ctx)); })
 	else begin
 	  if not eapply then failwith "make_apply_entry";
           if verbose then
@@ -678,7 +718,7 @@ let make_apply_entry env sigma (eapply,hnf,verbose) pri poly ?(name=PathAny) (c,
 	     poly = poly;
              pat = Some pat;
 	     name = name;
-             code = ERes_pf(c,cty,ctx) })
+             code = with_uid (ERes_pf(c,cty,ctx)); })
         end
     | _ -> failwith "make_apply_entry"
 
@@ -724,7 +764,7 @@ let make_unfold eref =
      poly = false;
      pat = None;
      name = PathHints [g];
-     code = Unfold_nth eref })
+     code = with_uid (Unfold_nth eref) })
 
 let make_extern pri pat tacast =
   let hdconstr = Option.map try_head_pattern pat in
@@ -733,7 +773,7 @@ let make_extern pri pat tacast =
      poly = false;
      pat = pat;
      name = PathAny;
-     code = Extern tacast })  
+     code = with_uid (Extern tacast) })  
 
 let make_mode ref m = 
   let ty = Global.type_of_global_unsafe ref in
@@ -749,14 +789,14 @@ let make_mode ref m =
 let make_trivial env sigma poly ?(name=PathAny) r =
   let c,ctx = fresh_global_or_constr env sigma poly r in
   let sigma = Evd.merge_context_set univ_flexible sigma ctx in
-  let t = hnf_constr env sigma (type_of env sigma c) in
+  let t = hnf_constr env sigma (unsafe_type_of env sigma c) in
   let hd = head_of_constr_reference (head_constr t) in
   let ce = mk_clenv_from_env env sigma None (c,t) in
   (Some hd, { pri=1;
 	      poly = poly;
               pat = Some (pi3 (Patternops.pattern_of_constr env ce.evd (clenv_type ce)));
 	      name = name;
-              code=Res_pf_THEN_trivial_fail(c,t,ctx) })
+              code= with_uid (Res_pf_THEN_trivial_fail(c,t,ctx)) })
 
 
 
@@ -771,9 +811,19 @@ let get_db dbname =
   try searchtable_map dbname
   with Not_found -> Hint_db.empty empty_transparent_state false
 
-let add_hint dbname hintlist = 
+let add_hint dbname hintlist =
+  let check (_, h) =
+    let () = if KNmap.mem h.code.uid !statustable then
+      error "Conflicting hint keys. This can happen when including \
+      twice the same module."
+    in
+    statustable := KNmap.add h.code.uid false !statustable
+  in
+  let () = List.iter check hintlist in
   let db = get_db dbname in
-  let db' = Hint_db.add_list hintlist db in
+  let env = Global.env () in
+  let sigma = Evd.from_env env in
+  let db' = Hint_db.add_list env sigma hintlist db in
     searchtable_add (dbname,db')
 
 let add_transparency dbname grs b =
@@ -816,7 +866,7 @@ type hint_obj = {
   hint_action : hint_action;
 }
 
-let cache_autohint (_, h) =
+let load_autohint _ (kn, h) =
   let name = h.hint_name in
   match h.hint_action with
   | CreateDB (b, st) -> searchtable_add (name, Hint_db.empty st b)
@@ -826,6 +876,16 @@ let cache_autohint (_, h) =
   | AddCut path -> add_cut name path
   | AddMode (l, m) -> add_mode name l m
 
+let open_autohint i (kn, h) =
+  if Int.equal i 1 then match h.hint_action with
+  | AddHints hints ->
+    let add (_, hint) = statustable := KNmap.add hint.code.uid true !statustable in
+    List.iter add hints
+  | _ -> ()
+
+let cache_autohint (kn, obj) =
+  load_autohint 1 (kn, obj); open_autohint 1 (kn, obj)
+
 let subst_autohint (subst, obj) =
   let subst_key gr =
     let (lab'', elab') = subst_global subst gr in
@@ -837,34 +897,36 @@ let subst_autohint (subst, obj) =
   let subst_hint (k,data as hint) =
     let k' = Option.smartmap subst_key k in
     let pat' = Option.smartmap (subst_pattern subst) data.pat in
-    let code' = match data.code with
+    let code' = match data.code.obj with
       | Res_pf (c,t,ctx) ->
           let c' = subst_mps subst c in
           let t' = subst_mps subst t in
-          if c==c' && t'==t then data.code else Res_pf (c', t',ctx)
+          if c==c' && t'==t then data.code.obj else Res_pf (c', t',ctx)
       | ERes_pf (c,t,ctx) ->
           let c' = subst_mps subst c in
           let t' = subst_mps subst t in
-          if c==c' && t'==t then data.code else ERes_pf (c',t',ctx)
+          if c==c' && t'==t then data.code.obj else ERes_pf (c',t',ctx)
       | Give_exact (c,t,ctx) ->
           let c' = subst_mps subst c in
 	  let t' = subst_mps subst t in
-          if c==c' && t'== t then data.code else Give_exact (c',t',ctx)
+          if c==c' && t'== t then data.code.obj else Give_exact (c',t',ctx)
       | Res_pf_THEN_trivial_fail (c,t,ctx) ->
           let c' = subst_mps subst c in
           let t' = subst_mps subst t in
-          if c==c' && t==t' then data.code else Res_pf_THEN_trivial_fail (c',t',ctx)
+          if c==c' && t==t' then data.code.obj else Res_pf_THEN_trivial_fail (c',t',ctx)
       | Unfold_nth ref ->
           let ref' = subst_evaluable_reference subst ref in
-          if ref==ref' then data.code else Unfold_nth ref'
+          if ref==ref' then data.code.obj else Unfold_nth ref'
       | Extern tac ->
 	  let tac' = Tacsubst.subst_tactic subst tac in
-	  if tac==tac' then data.code else Extern tac'
+	  if tac==tac' then data.code.obj else Extern tac'
     in
     let name' = subst_path_atom subst data.name in
+    let uid' = subst_kn subst data.code.uid in
     let data' =
-      if data.pat==pat' && data.name == name' && data.code==code' then data
-      else { data with pat = pat'; name = name'; code = code' }
+      if data.code.uid == uid' && data.pat == pat' &&
+        data.name == name' && data.code.obj == code' then data
+      else { data with pat = pat'; name = name'; code = { obj = code'; uid = uid' } }
     in
     if k' == k && data' == data then hint else (k',data')
   in
@@ -896,7 +958,8 @@ let classify_autohint obj =
 let inAutoHint : hint_obj -> obj =
   declare_object {(default_object "AUTOHINT") with
                     cache_function = cache_autohint;
-		    load_function = (fun _ -> cache_autohint);
+		    load_function = load_autohint;
+		    open_function = open_autohint;
 		    subst_function = subst_autohint;
 		    classify_function = classify_autohint; }
 
@@ -999,7 +1062,7 @@ let default_prepare_hint_ident = Id.of_string "H"
 
 exception Found of constr * types
 
-let prepare_hint check env init (sigma,c) =
+let prepare_hint check (poly,local) env init (sigma,c) =
   let sigma = Typeclasses.resolve_typeclasses ~fail:false env sigma in
   (* We re-abstract over uninstantiated evars.
      It is actually a bit stupid to generalize over evars since the first
@@ -1012,7 +1075,7 @@ let prepare_hint check env init (sigma,c) =
       (* We skip the test whether args is the identity or not *)
       let t = Evarutil.nf_evar sigma (existential_type sigma ev) in
       let t = List.fold_right (fun (e,id) c -> replace_term e id c) !subst t in
-      if not (Int.Set.is_empty (free_rels t)) then
+      if not (closed0 c) then
 	error "Hints with holes dependent on a bound variable not supported.";
       if occur_existential t then
 	(* Not clever enough to construct dependency graph of evars *)
@@ -1029,13 +1092,18 @@ let prepare_hint check env init (sigma,c) =
   let c' = iter c in
     if check then Evarutil.check_evars (Global.env()) Evd.empty sigma c';
     let diff = Univ.ContextSet.diff (Evd.universe_context_set sigma) (Evd.universe_context_set init) in
-      IsConstr (c', diff)
+    if poly then IsConstr (c', diff)
+    else if local then IsConstr (c', diff)
+    else (Global.push_context_set false diff;
+	  IsConstr (c', Univ.ContextSet.empty))
 
 let interp_hints poly =
   fun h ->
-  let f c =
-    let evd,c = Constrintern.interp_open_constr (Global.env()) Evd.empty c in
-      prepare_hint true (Global.env()) Evd.empty (evd,c) in
+  let env = (Global.env()) in
+  let sigma = Evd.from_env env in
+  let f poly c =
+    let evd,c = Constrintern.interp_open_constr env sigma c in
+      prepare_hint true (poly,false) (Global.env()) Evd.empty (evd,c) in
   let fref r =
     let gr = global_with_alias r in
     Dumpglob.add_glob (loc_of_reference r) gr;
@@ -1048,7 +1116,7 @@ let interp_hints poly =
     | HintsReference c ->
       let gr = global_with_alias c in
 	(PathHints [gr], poly, IsGlobRef gr)
-    | HintsConstr c -> (PathAny, poly, f c)
+    | HintsConstr c -> (PathAny, poly, f poly c)
   in
   let fres (pri, b, r) =
     let path, poly, gr = fi r in
@@ -1083,7 +1151,8 @@ let add_hints local dbnames0 h =
   if String.List.mem "nocore" dbnames0 then
     error "The hint database \"nocore\" is meant to stay empty.";
   let dbnames = if List.is_empty dbnames0 then ["core"] else dbnames0 in
-  let env = Global.env() and sigma = Evd.empty in
+  let env = Global.env() in
+  let sigma = Evd.from_env env in
   match h with
   | HintsResolveEntry lhints -> add_resolves env sigma lhints local dbnames
   | HintsImmediateEntry lhints -> add_trivials env sigma lhints local dbnames
@@ -1103,7 +1172,7 @@ let expand_constructor_hints env sigma lems =
 	  (fun i -> IsConstr (mkConstructU ((ind,i+1),u), 
 			      Univ.ContextSet.empty))
     | _ ->
-	[prepare_hint false env sigma (evd,lem)]) lems
+	[prepare_hint false (false,true) env sigma (evd,lem)]) lems
 
 (* builds a hint database from a constr signature *)
 (* typically used with (lid, ltyp) = pf_hyps_types <some goal> *)
@@ -1111,8 +1180,8 @@ let expand_constructor_hints env sigma lems =
 let add_hint_lemmas env sigma eapply lems hint_db =
   let lems = expand_constructor_hints env sigma lems in
   let hintlist' =
-    List.map_append (make_resolves env sigma (eapply,true,false) None true) lems in
-  Hint_db.add_list hintlist' hint_db
+    List.map_append (make_resolves env sigma (eapply,true,false) None false) lems in
+  Hint_db.add_list env sigma hintlist' hint_db
 
 let make_local_hint_db env sigma ts eapply lems =
   let sign = Environ.named_context env in
@@ -1122,7 +1191,7 @@ let make_local_hint_db env sigma ts eapply lems =
   in
   let hintlist = List.map_append (make_resolve_hyp env sigma) sign in
   add_hint_lemmas env sigma eapply lems
-    (Hint_db.add_list hintlist (Hint_db.empty ts false))
+    (Hint_db.add_list env sigma hintlist (Hint_db.empty ts false))
 
 let make_local_hint_db = 
   if Flags.profile then
@@ -1146,13 +1215,14 @@ let make_db_list dbnames =
 (*                    Functions for printing the hints                    *)
 (**************************************************************************)
 
-let pr_autotactic =
-  function
-  | 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")
+let pr_hint_elt (c, _, _) = pr_constr c
+
+let pr_hint h = match h.obj with
+  | 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 =
@@ -1163,11 +1233,11 @@ let pr_autotactic =
       in
       (str "(*external*) " ++ Pptactic.pr_glob_tactic env tac)
 
-let pr_hint (id, v) =
-  (pr_autotactic v.code ++ str"(level " ++ int v.pri ++ str", id " ++ int id ++ str ")" ++ spc ())
+let pr_id_hint (id, v) =
+  (pr_hint v.code ++ str"(level " ++ int v.pri ++ str", id " ++ int id ++ str ")" ++ spc ())
 
 let pr_hint_list hintlist =
-  (str "  " ++ hov 0 (prlist pr_hint hintlist) ++ fnl ())
+  (str "  " ++ hov 0 (prlist pr_id_hint hintlist) ++ fnl ())
 
 let pr_hints_db (name,db,hintlist) =
   (str "In the database " ++ str name ++ str ":" ++
@@ -1266,3 +1336,27 @@ let pr_searchtable () =
   in
   Hintdbmap.fold fold !searchtable (mt ())
 
+let print_mp mp =
+  try
+    let qid = Nametab.shortest_qualid_of_module mp in
+    str " from "  ++ pr_qualid qid
+  with Not_found -> mt ()
+
+let is_imported h = try KNmap.find h.uid !statustable with Not_found -> true
+
+let warn h x =
+  let hint = pr_hint h in
+  let (mp, _, _) = KerName.repr h.uid in
+  let () = msg_warning (str "Hint used but not imported: " ++ hint ++ print_mp mp) in
+  Proofview.tclUNIT x
+
+let run_hint tac k = match !warn_hint with
+| `LAX -> k tac.obj
+| `WARN ->
+  if is_imported tac then k tac.obj
+  else Proofview.tclBIND (k tac.obj) (fun x -> warn tac x)
+| `STRICT ->
+  if is_imported tac then k tac.obj
+  else Proofview.tclZERO (UserError ("", (str "Tactic failure.")))
+
+let repr_hint h = h.obj