From fe143846ecaa62058f652ed65874270aae5750e8 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Wed, 17 Apr 2024 13:19:41 +0200 Subject: [PATCH] Adapt to coq/coq#18938 (EConstr.ERelevance) --- src/coq.ml | 2 +- src/coq.mli | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/coq.ml b/src/coq.ml index 9463c78..292e4ff 100644 --- a/src/coq.ml +++ b/src/coq.ml @@ -17,7 +17,7 @@ open Proofview.Notations type tactic = unit Proofview.tactic -let mkArrow x y = mkArrow x Sorts.Relevant y +let mkArrow x y = mkArrow x ERelevance.relevant y (* The kernel will fix the relevance if needed. Also as an equality tactic we probably are only called on relevant terms. *) diff --git a/src/coq.mli b/src/coq.mli index 0f68faf..add9ccf 100644 --- a/src/coq.mli +++ b/src/coq.mli @@ -42,7 +42,7 @@ val mk_letin : string -> EConstr.constr -> EConstr.constr Proofview.tactic val tclRETYPE : EConstr.constr -> unit Proofview.tactic -val decomp_term : Evd.evar_map -> EConstr.constr -> (EConstr.constr , EConstr.types, EConstr.ESorts.t, EConstr.EInstance.t) Constr.kind_of_term +val decomp_term : Evd.evar_map -> EConstr.constr -> (EConstr.constr , EConstr.types, EConstr.ESorts.t, EConstr.EInstance.t, EConstr.ERelevance.t) Constr.kind_of_term (** {2 Bindings with Coq' Standard Library} *)