diff --git a/src/Common/Tactics/hint_db_extra_plugin.mlg.v819 b/src/Common/Tactics/hint_db_extra_plugin.mlg.v819
index ab3e3e98..ca52411a 100644
--- a/src/Common/Tactics/hint_db_extra_plugin.mlg.v819
+++ b/src/Common/Tactics/hint_db_extra_plugin.mlg.v819
@@ -16,5 +16,5 @@ TACTIC EXTEND foreach_db
 
 TACTIC EXTEND addto_db
   | [ "add" constr(name) "to" ne_preident_list(l) ]  ->
-     { WITH_DB.add_resolve_to_db (Hints.hint_constr (name, None)) l }
+     { WITH_DB.add_resolve_to_db name l }
        END
diff --git a/src/Common/Tactics/hint_db_extra_tactics.ml.v819 b/src/Common/Tactics/hint_db_extra_tactics.ml.v819
index da53d0b0..39e64ab8 100644
--- a/src/Common/Tactics/hint_db_extra_tactics.ml.v819
+++ b/src/Common/Tactics/hint_db_extra_tactics.ml.v819
@@ -41,10 +41,16 @@ module WITH_DB =
       end
 
   let add_resolve_to_db lem db =
-    Proofview.Goal.enter begin
-	fun gl ->
-	let _ = Hints.add_hints ~locality:Hints.Local db (Hints.HintsResolveEntry [({ Typeclasses.hint_priority = Some 1 ; Typeclasses.hint_pattern = None }, true, lem)]) in
-	tclIDTAC
-      end
+    Proofview.Goal.enter begin fun gl ->
+      let sigma = Proofview.Goal.sigma gl in
+      (* Tolerate applications to please tclABSTRACT in a section *)
+      let lem, _ = EConstr.decompose_app sigma lem in
+      match EConstr.destRef sigma lem with
+      | gr, _ ->
+        let lem = Hints.hint_globref gr in
+        let () = Hints.add_hints ~locality:Hints.Local db (Hints.HintsResolveEntry [({ Typeclasses.hint_priority = Some 1 ; Typeclasses.hint_pattern = None }, true, lem)]) in
+        tclIDTAC
+      | exception Constr.DestKO -> tclFAIL (Pp.str "Cannot add non-global to hint database")
+    end
 
 end