Adapt to coq/coq#18327 (projection opacity) (impermeable#41)

src/wp_auto.ml

@@ -81,9 +81,10 @@ let exact (h: hint): unit tactic =
 (**
   Same function as {! Auto.exists_evaluable_reference}
 *)
-let exists_evaluable_reference (env: Environ.env) (evaluable_ref: Tacred.evaluable_global_reference): bool = match evaluable_ref with
-  | Tacred.EvalConstRef _ -> true
-  | Tacred.EvalVarRef v -> try ignore(Environ.lookup_named v env); true with Not_found -> false
+let exists_evaluable_reference (env: Environ.env) (evaluable_ref: Names.Evaluable.t): bool = match evaluable_ref with
+  | Evaluable.EvalConstRef _ -> true
+  | Evaluable.EvalProjectionRef _ -> true
+  | Evaluable.EvalVarRef v -> try ignore(Environ.lookup_named v env); true with Not_found -> false
 
 (* All the definitions below are inspired by the coq-core hidden library (i.e not visible in the API) but modified for Waterproof *)
 
@@ -313,4 +314,4 @@ let wp_auto (log: bool) (n: int) (lems: Tactypes.delayed_open_constr list) (dbna
   This function acts the same as {! wp_auto} but will fail if all proof found contain at least one must-use lemma that is unused or one hint that is in the [forbidden] list.
 *)
 let rwp_auto (log: bool) (n: int) (lems: Tactypes.delayed_open_constr list) (dbnames: hint_db_name list) (must_use_tactics: Pp.t list) (forbidden_tactics: Pp.t list): trace tactic =
-  gen_wp_auto log ~n lems (Some dbnames) must_use_tactics forbidden_tactics
+  gen_wp_auto log ~n lems (Some dbnames) must_use_tactics forbidden_tactics

src/wp_auto.mli

@@ -21,7 +21,7 @@ open Backtracking
 (**
   Same function as {! Auto.exists_evaluable_reference}
 *)
-val exists_evaluable_reference : Environ.env -> Tacred.evaluable_global_reference -> bool
+val exists_evaluable_reference : Environ.env -> Names.Evaluable.t -> bool
 
 (**
   Prints "idtac" if the [log] field is [true]
@@ -87,4 +87,4 @@ val rwp_auto :
   string list ->
   Pp.t list ->
   Pp.t list ->
-  Backtracking.trace Proofview.tactic
+  Backtracking.trace Proofview.tactic