Stream: Coq devs & plugin devs

Topic: Is master broken?


view this post on Zulip Rodolphe Lepigre (Apr 24 2024 at 09:17):

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

view this post on Zulip Gaëtan Gilbert (Apr 24 2024 at 09:21):

yes

view this post on Zulip Gaëtan Gilbert (Apr 24 2024 at 10:44):

https://github.com/coq/coq/pull/18974

view this post on Zulip Hugo Herbelin (Apr 24 2024 at 11:32):

The "Unsafe" there is expected? Or is it a "hot" fix?

view this post on Zulip Gaëtan Gilbert (Apr 24 2024 at 11:34):

who knows


Last updated: Oct 13 2024 at 01:02 UTC