coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Typeclasses vs canonical instances

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