From eb307d8faa80194b1e6485329836f27effb3dc6a Mon Sep 17 00:00:00 2001 From: Rodolphe Lepigre Date: Wed, 3 Apr 2024 13:11:11 +0200 Subject: [PATCH] Adapt to coq/coq#18546. (#48) --- src/wp_auto.ml | 2 +- src/wp_auto.mli | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/wp_auto.ml b/src/wp_auto.ml index a92d527c..1c072320 100644 --- a/src/wp_auto.ml +++ b/src/wp_auto.ml @@ -81,7 +81,7 @@ let exact (h: hint): unit tactic = (** Same function as {! Auto.exists_evaluable_reference} *) -let exists_evaluable_reference (env: Environ.env) (evaluable_ref: Names.Evaluable.t): bool = match evaluable_ref with +let exists_evaluable_reference (env: Environ.env) (evaluable_ref: 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 diff --git a/src/wp_auto.mli b/src/wp_auto.mli index fd96007f..e3b11f01 100644 --- a/src/wp_auto.mli +++ b/src/wp_auto.mli @@ -21,7 +21,7 @@ open Backtracking (** Same function as {! Auto.exists_evaluable_reference} *) -val exists_evaluable_reference : Environ.env -> Names.Evaluable.t -> bool +val exists_evaluable_reference : Environ.env -> Evaluable.t -> bool (** Prints "idtac" if the [log] field is [true]