Merge pull request #139 from SkySkimmer/erelevance

Adapt to coq/coq#18938 (EConstr.ERelevance)
coq-community · Apr 23, 2024 · d29656d · d29656d
2 parents d3f4d88 + fe14384
commit d29656d
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git 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
@@ -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}  *)