coq-club AT inria.fr

Subject: The Coq mailing list

List archive

From: Julien Narboux <jnarboux AT narboux.fr>
To: Coq Club <coq-club AT inria.fr>
Subject: [Coq-Club] typeclass resolution and unfold
Date: Thu, 6 Jul 2017 17:12:31 +0200
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jnarboux AT narboux.fr; spf=None smtp.mailfrom=jnarboux AT narboux.fr; spf=None smtp.helo=postmaster AT mail-pg0-f48.google.com
Ironport-phdr: 9a23:rWBnfBz7B0yJJ6LXCy+O+j09IxM/srCxBDY+r6Qd1OkQIJqq85mqBkHD//Il1AaPBtSEraocw8Pt8InYEVQa5piAtH1QOLdtbDQizfssogo7HcSeAlf6JvO5JwYzHcBFSUM3tyrjaRsdF8nxfUDdrWOv5jAOBBr/KRB1JuPoEYLOksi7ze6/9pnRbglSmDaxfa55IQmrownWqsQYm5ZpJLwryhvOrHtIeuBWyn1tKFmOgRvy5dq+8YB6/ShItP0v68BPUaPhf6QlVrNYFygpM3o05MLwqxbOSxaE62YGXWUXlhpIBBXF7A3/U5zsvCb2qvZx1S+HNsDtU7s6RSqt4LtqSB/wiScIKTg58H3MisdtiK5XuQ+tqwBjz4LRZoyeKfhwcb7Hfd4CRWRPUMVfWTFfDIygdIYAFfYNMPxCooXhu1cDrx2zDhSsCuP1zT9Ig2f706kn0+QlEAHJwgogFM8WvnvOttX6L6ASUf26zaLVyjjDbfVW1i3n6IfTdRAhvP6NUKl2ccXL00kgDATFjkifqID/MTOVzP0Avm6G5ORjTeKik2wqpg5rrjSy2MshipPFi4Ebx1ze+ih0w4A4LsCiRkFhe96rCp5QujmaN4RoRsMiRHlluCMgxb0HvZ63ZTAKyJs7yxLGZfyKfIuF7gjsVOaWJjd4i3Zld6ylixmu9kigz/XwVsiy0FlUsipIitvBu38X2xDO9MSKSuFx80Sv1DqV2A3e6flIIUUumqraL54hzKQwlp0WsUnbHC/2nl/5jLWNeUUj5+ip5P/qYrP8qZ+GLIB0jRz+M6s0lsyxG+Q0KhIOUHSD+eSgyL3j+lX0T6lNjv0vi6XWrJTaJdkAqaOiGA9U0oMj6w6lADu80dQYm2MHLFNfdx6dgYjpIQKGHPetJvCmy3+ojT0jk/vBJ/jqBojHBnnFirboO7hnvR1y0g02mPJC45NZDPknKej5XVLh/IjaCBYjOQup087hAc930Z4OH2yVVPzKeJjOuEOFs7p8a9KHY5UY7XOkc6Ao

Hello,

I have defined a type class, and definitions depending on fields of the type class.

I would like to write a tactic which unfold the definition given as an argument.

How can I do that ?

Here is a small test case:

Class foo:= {

A : Type;

B: A -> A -> Prop;

babar a b := B a b /\ B b a;

Ltac myunfold t := unfold t.

Section bar.

Context `{Ax:foo}.

Lemma titi : forall a b, babar a b.

Proof.

intros.

(* unfold babar. works *)

myunfold babar.

(* In nested Ltac calls to "myunfold" and "unfold t", last call failed.

Error: Ltac variable t is bound to babar which cannot be coerced to

an evaluable reference. *)

Julien

[Coq-Club] typeclass resolution and unfold, Julien Narboux, 07/06/2017
- Re: [Coq-Club] typeclass resolution and unfold, Pierre Courtieu, 07/06/2017