I'm getting:
File "plugins/ltac2/tac2core.ml", line 834, characters 93-112:
834 | define "constr_binder_relevance" (repr_ext val_binder @-> ret relevance) @@ fun (na, _) -> na.binder_relevance
^^^^^^^^^^^^^^^^^^^
Error: This expression has type EConstr.ERelevance.t = Evd.erelevance
but an expression was expected of type Sorts.relevance
yes
https://github.com/coq/coq/pull/18974
The "Unsafe" there is expected? Or is it a "hot" fix?
who knows
Last updated: Oct 13 2024 at 01:02 UTC