Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Typeclasses vs canonical instances

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Typeclasses vs canonical instances


Chronological Thread 
  • 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



Archive powered by MHonArc 2.6.18.

Top of Page