coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Interaction between Setoids and Canonical Structures

From: Cyril Cohen <cohen AT crans.org>
To: Matthieu Sozeau <mattam AT mattam.org>
Cc: Carsten Varming <varming AT cmu.edu>, Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Interaction between Setoids and Canonical Structures
Date: Wed, 15 Dec 2010 15:19:28 +0100

Hi,

Le 14/12/2010 19:18, Matthieu Sozeau a �crit :
> The problem is that the unification (noted ~) fails on: (sort' (str_str'
> ?1)) ~ (sort T).
> Note that in the first term we don't know what the existential ?1 is.

Thank you Matthieu for this explanation. When I have the time, I might
try to fix my problem by triggering a weaker unification (sort' ?1) ~
(sort T) which would succeed thanks to cannonical structure recognition.

Cheers,
--
Cyril

[Coq-Club] Interaction between Setoids and Canonical Structures, Cyril Cohen
- Re: [Coq-Club] Interaction between Setoids and Canonical Structures, Cyril Cohen
  - Re: [Coq-Club] Interaction between Setoids and Canonical Structures, Carsten Varming
    - Re: [Coq-Club] Interaction between Setoids and Canonical Structures, Cyril Cohen
      - Re: [Coq-Club] Interaction between Setoids and Canonical Structures, Carsten Varming
        
        Re: [Coq-Club] Interaction between Setoids and Canonical Structures, Cyril Cohen
        
        Re: [Coq-Club] Interaction between Setoids and Canonical Structures, Matthieu Sozeau
        
        Re: [Coq-Club] Interaction between Setoids and Canonical Structures, Cyril Cohen