Stream: Coq devs & plugin devs

Topic: ✔ EConstr.Vars.subst_var

view this post on Zulip Jason Gross (Sep 26 2022 at 15:34):

Has EConstr.Vars.subst_var changed types recently? mit-plv/rewriter builds find on CI, but when I try to build it locally against https://github.com/coq/coq/pull/16508 it fails with

File "src/Rewriter/Util/plugins/inductive_from_elim.ml", line 43, characters 54-58:
43 |       EConstr.to_constr sigma (EConstr.Vars.subst_var name cty)
                                                           ^^^^
Error: This expression has type Names.Id.t
       but an expression was expected of type Evd.evar_map

view this post on Zulip Gaëtan Gilbert (Sep 26 2022 at 15:34):

yes

view this post on Zulip Gaëtan Gilbert (Sep 26 2022 at 15:34):

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

view this post on Zulip Jason Gross (Sep 26 2022 at 15:35):

Oh, I guess my branch is not up to date with rewriter's master

view this post on Zulip Notification Bot (Sep 26 2022 at 15:35):

Jason Gross has marked this topic as resolved.

Last updated: Dec 01 2023 at 04:01 UTC