coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] mysterious evar unification failure after subst

From: Jonathan Leivent <jonikelee AT gmail.com>
To: Coq Club <coq-club AT inria.fr>
Subject: [Coq-Club] mysterious evar unification failure after subst
Date: Tue, 20 Oct 2015 19:32:08 -0400
Authentication-results: mail2-smtp-roc.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-f176.google.com
Ironport-phdr: 9a23:XT2T3hGfNtBY81kjGa9PuJ1GYnF86YWxBRYc798ds5kLTJ75r8mwAkXT6L1XgUPTWs2DsrQf27eQ6/mrAzdIyK3CmU5BWaQEbwUCh8QSkl5oK+++Imq/EsTXaTcnFt9JTl5v8iLzG0FUHMHjew+a+SXqvnYsExnyfTB4Ov7yUtaLyZ/niqbqotaJOE1hv3mUX/BbFF2OtwLft80b08NJC50a7V/3mEZOYPlc3mhyJFiezF7W78a0+4N/oWwL46pyv+YJa6jxfrw5QLpEF3xmdjltvIy4gzCYElDKvidUEjhO00kAPw+QxxbjFrz1ryGy4uF6wWyROdD8ZbEyQzWrqalxHkzGkiACYhw+9mjLisV2xIZWoQysoQA3l4zTZoCWOf5zc4vSeNobQSxKWcMHBH8JOZ+1c4ZaV7lJBu1ftYSo4gZWoA==

Why does the second reflexivity fail in the following?:

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?*)

It seems to me that, since the substitution maps of the two evars are identical {n:=1}, then the unification should be allowed. Is there something that would go wrong if the unification was allowed?

I'm using recent 8.5 version 7d6d9c5

-- Jonathan

[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