More reasonable implementation of add_resolve_to_db. (#109)

We stop relying on Hints.hint_constr and only add terms that look like a
global reference. All callers are respecting this precondition as they go
through a variant of abstract.

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

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