coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] mysterious evar unification failure after subst

From: Jonathan Leivent <jonikelee AT gmail.com>
To: Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] mysterious evar unification failure after subst
Date: Tue, 20 Oct 2015 19:56:31 -0400
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=jonikelee AT gmail.com; spf=Pass smtp.mailfrom=jonikelee AT gmail.com; spf=None smtp.helo=postmaster AT mail-qk0-f169.google.com
Ironport-phdr: 9a23:q0yWWhdo/9q3SZLu9q3+gmVAlGMj4u6mDksu8pMizoh2WeGdxc69Zh7h7PlgxGXEQZ/co6odzbGG7ua4ACdaut6oizMrTt9lb1c9k8IYnggtUoauKHbQC7rUVRE8B9lIT1R//nu2YgB/Ecf6YEDO8DXptWZBUiv2OQc9HOnpAIma153xjLDvvcWKKF8TzBOGIppMbzyO5T3LsccXhYYwYo0Q8TDu5kVyRuJN2GlzLkiSlRuvru25/Zpk7jgC86l5r50IeezAcq85Vb1VCig9eyBwvZWz9EqLcQzazXwFGk4SjxAAVwPC9VTxWor7mir8rOt0nieAa57YV7cxDBal6a53SBbuwAMKNiA09n2f3s53iqNYrRasqjRwxofVZMeeM/8oLfCVRs8TWWcUBpUZbCdGGI7pKtJXV+c=

Answering my own question:

I think this is another instance of bug 3141. So, maybe a workaround is to use instantiate before unifying...

-- Jonathan

On 10/20/2015 07:32 PM, Jonathan Leivent wrote:

Goal forall n, n=1 -> exists x y : nat, x=y.
intros.
do 2 eexists.
reflexivity. (*this works, but...*)
Undo.
subst.
Fail reflexivity. (*why does this fail?*)

[Coq-Club] mysterious evar unification failure after subst, Jonathan Leivent, 10/21/2015
- Re: [Coq-Club] mysterious evar unification failure after subst, Jonathan Leivent, 10/21/2015
  - Re: [Coq-Club] mysterious evar unification failure after subst, Beta Ziliani, 10/21/2015
- Re: [Coq-Club] mysterious evar unification failure after subst, Hugo Herbelin, 10/21/2015