Add a more general quote construction

"quote f [...] in c using t" will call t (must be an ltac function)
with a X (of form "f x" or "f vm x") such that X converts to c. In
particular,

  match goal with
    | H : ?x |- _ =>
      quote f in x using (fun X => change X in H)
  end

may be used as an equivalent of plain quote that acts on an
hypothesis. The construction can be used in a more general way,
though.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12037 85f007b7-540e-0410-9357-904b9bb8a0f7

0 files changed, 0 insertions, 0 deletions