Skip to content

Commit 9b27f1e

Browse files
authored
Merge pull request #1136 from SkySkimmer/set-leq-noenv
Adapt to rocq-prover/rocq#20069 (set_leq_sort doesn't need an env)
2 parents 264d924 + c407be4 commit 9b27f1e

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

template-coq/src/tm_util.ml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -246,7 +246,7 @@ module RetypeMindEntry =
246246
let _, indsort = Reduction.dest_arity env oib.mind_entry_arity in
247247
let indsort = EConstr.ESorts.make indsort in
248248
(* Hacky, but we don't have a good way to enfore max() <= max() constraints yet *)
249-
let evm = try Evd.set_leq_sort env evm cstrsort indsort with e -> evm in
249+
let evm = try Evd.set_leq_sort evm cstrsort indsort with e -> evm in
250250
evm)
251251
evm mind.mind_entry_inds
252252
in

0 commit comments

Comments
 (0)