coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Enrico Tassi <enrico.tassi AT inria.fr>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Typeclasses vs canonical instances
- Date: Fri, 29 Apr 2016 11:15:02 +0200
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=enrico.tassi AT inria.fr; spf=None smtp.mailfrom=gares AT fettunta.org; spf=None smtp.helo=postmaster AT fettunta.org
- Ironport-phdr: 9a23:h6DENhb55YgOVKZcXbMhWqf/LSx+4OfEezUN459isYplN5qZpc+9bnLW6fgltlLVR4KTs6sC0LqG9fC+EjRbqb+681k8M7V0HycfjssXmwFySOWkMmbcaMDQUiohAc5ZX0Vk9XzoeWJcGcL5ekGA6ibqtW1aJBzzOEJPK/jvHcaK1oLsh7D0q8OYO14ArQH+SI0xBS3+lR/WuMgSjNkqAYcK4TyNnEF1ff9Lz3hjP1OZkkW0zM6x+Jl+73YY4Kp5pIYTGZn9Kq8/VPlTCCksG2Ez/szi8xfZHiWV4X5Jf2MMkxFPSzTM9wr7FsP8tDH7ve07xCCBJszeTLYuWD3k4b09G0ygszsOKzNsqDKfscd3lq8O+B8=
On Thu, Apr 28, 2016 at 02:11:02AM +0000, Jason Gross wrote:
> If you have [Definition foo := Set.] and you can't get multiple successes
> out of [unify foo foo] (where the second success comes from unfolding both
> [foo]s), which I suspect you can't, then the backtracking of unification
> isn't accessible from Ltac-land.
Yep, maybe what was not clear in my answer is that CS resolution takes
place in the middle of unification, so one can use the backtracking
facility of the enclosing algorithm to bring backtracking to CS
resolution.
Best,
--
Enrico Tassi
- [Coq-Club] Typeclasses vs canonical instances, Igor Zhirkov, 04/24/2016
- Re: [Coq-Club] Typeclasses vs canonical instances, Gregory Malecha, 04/25/2016
- Re: [Coq-Club] Typeclasses vs canonical instances, Guillaume Melquiond, 04/26/2016
- Re: [Coq-Club] Typeclasses vs canonical instances, Jonathan Leivent, 04/27/2016
- Re: [Coq-Club] Typeclasses vs canonical instances, Gregory Malecha, 04/27/2016
- Re: [Coq-Club] Typeclasses vs canonical instances, Pierre-Marie Pédrot, 04/27/2016
- Re: [Coq-Club] Typeclasses vs canonical instances, Enrico Tassi, 04/27/2016
- Re: [Coq-Club] Typeclasses vs canonical instances, Jonathan Leivent, 04/28/2016
- Re: [Coq-Club] Typeclasses vs canonical instances, Jason Gross, 04/28/2016
- Re: [Coq-Club] Typeclasses vs canonical instances, Enrico Tassi, 04/29/2016
- Re: [Coq-Club] Typeclasses vs canonical instances, Enrico Tassi, 04/27/2016
- Re: [Coq-Club] Typeclasses vs canonical instances, Pierre-Marie Pédrot, 04/27/2016
- Re: [Coq-Club] Typeclasses vs canonical instances, Gregory Malecha, 04/27/2016
- Re: [Coq-Club] Typeclasses vs canonical instances, Jonathan Leivent, 04/27/2016
- Re: [Coq-Club] Typeclasses vs canonical instances, Guillaume Melquiond, 04/26/2016
- Re: [Coq-Club] Typeclasses vs canonical instances, Gregory Malecha, 04/25/2016
Archive powered by MHonArc 2.6.18.