`context` expression in Coq

Question

I am trying to understand 'context' expression (opposed to context pattern). In the manual it is described as:

context ident [ expr ]

ident must denote a context variable bound by a context pattern of a match expression. This expression evaluates replaces the hole of the value of ident by the value of expr.

Could somebody share an example illustrating the usage of this construct? I guess it must involve match using context pattern and then abovementioned form to use matched context.

I think it is a "hole". Anyway, this is what it says in the manual coq.inria.fr/refman/ltac.html#hevea_default856 — krokodil

Jason Gross Jason Gross · Accepted Answer · 2017-11-19T06:10:42

Here is an example that replaces fst (a, _) with a and snd (_, b) with b, but doesn't touch fst and snd applied to anything other than pair:

Ltac unfold_proj_pair :=
    repeat match goal with
           | [ |- context G[fst (?a, _)] ]
             => let G' := context G[a] in change G'
           | [ |- context G[snd (_, ?b)] ]
             => let G' := context G[b] in change G'
           end.

(Note that cbn [fst snd] is a simpler way to do this, and that also works under binders.)

`context` expression in Coq

1 Answers