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
Oh, I guess my branch is not up to date with rewriter's master
Jason Gross has marked this topic as resolved.
Last updated: Feb 06 2023 at 18:03 UTC