Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.
The following code worked fine in Coq 8.14, but no longer works in Coq 8.15:
From Coq Require Import String.
From Coq.ssr Require Export ssreflect.
Set Mangle Names.
Set Mangle Names Prefix "_".
Inductive val :=
| PairV (v1 v2 : val).
Inductive expr :=
| Call (e1 : expr) (e2 : expr)
| If (e0 e1 e2 : expr).
Section test.
Context (subst : string -> val -> expr -> expr).
Lemma to_expr_subst x v e :
subst x v e = subst x v e.
Proof.
elim: e => /= [^ e].
It now says (when running the [^ e] pattern)
Error: e_0 already used
Given that it passed in 8.14 with and without name mangling, I would expect this code to be stable under changes to automatic naming. Hence I am surprised that it no longer works.
Coq Version
The Coq Proof Assistant, version 8.15.2
compiled with OCaml 4.14.0
Alizter
commented
2 years ago
Description of the problem
The following code worked fine in Coq 8.14, but no longer works in Coq 8.15:
It now says (when running the
[^ e]pattern)Given that it passed in 8.14 with and without name mangling, I would expect this code to be stable under changes to automatic naming. Hence I am surprised that it no longer works.
Coq Version