The Coq mailing list

[Robbert Krebbers <mailinglists AT robbertkrebbers.nl>]

I was looking for some means to do some lightweight reification without 
the need for writing an OCaml plugin or the using Ltac/type 
classes/canonical structures (which are too slow), so I stumbled on the 
[quote] tactic. Unfortunately, I cannot get it to work for polymorphic 
data types like lists, see below.

Does anyone know whether I am doing something wrong, or whether [quote] 
just does not support my use case below.

======================================

Require Import Quote.

Inductive formula : Type :=
  | f_nil : formula
  | f_app : formula -> formula -> formula
  | f_atom : index -> formula.

Fixpoint interp_f {A} (vm : varmap (list A)) (f:formula) : list A :=
  match f with
  | f_nil => nil
  | f_app f1 f2 => interp_f vm f1 ++ interp_f vm f2
  | f_atom i => varmap_find nil i vm
  end.

Goal forall x : list nat, True.
intros.

quote interp_f in (x ++ x ++ nil)%list using (fun x => idtac x).
(* Yields nonsense *)

quote (@interp_f nat) in (x ++ x ++ nil)%list using (fun x => idtac x).
(* Fails with Syntax error: [prim:ident] expected after 'quote' (in 
[tactic:simple_tactic]). *)