Dnets now consider axioms as being opaque for pattern recognition.

1 files changed, 4 insertions, 4 deletions

diff --git a/tactics/hints.mli b/tactics/hints.mli
index 0b9da27ab3..e061bd7648 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -134,18 +134,18 @@ module Hint_db :
     (** All hints associated to the reference, respecting modes if evars appear in the
         arguments and using the discrimination net.
         Returns a [ModeMismatch] if there are declared modes and none matches. *)
-    val map_eauto : evar_map -> secvars:Id.Pred.t -> (GlobRef.t * constr array) -> constr -> t -> FullHint.t list with_mode
+    val map_eauto : env -> evar_map -> secvars:Id.Pred.t -> (GlobRef.t * constr array) -> constr -> t -> FullHint.t list with_mode
 
     (** All hints associated to the reference.
         Precondition: no evars should appear in the arguments, so no modes
         are checked. *)
-    val map_auto : evar_map -> secvars:Id.Pred.t ->
+    val map_auto : env -> evar_map -> secvars:Id.Pred.t ->
        (GlobRef.t * constr array) -> constr -> t -> FullHint.t list
 
     val add_one : env -> evar_map -> hint_entry -> t -> t
     val add_list : env -> evar_map -> hint_entry list -> t -> t
-    val remove_one : GlobRef.t -> t -> t
-    val remove_list : GlobRef.t list -> t -> t
+    val remove_one : Environ.env -> GlobRef.t -> t -> t
+    val remove_list : Environ.env -> GlobRef.t list -> t -> t
     val iter : (GlobRef.t option ->
                 hint_mode array list -> FullHint.t list -> unit) -> t -> unit