Usage of "red in |- *": What does bar hyphen star mean?

Question

In a lot of Coq code, like in the definition of sets in the standard library, I've seen this sort of notation:

 red in |- *.

What does the |-* (bar-hyphen-star) mean?

My searching hasn't turned up any results, but it's hard to search for punctuation, so please excuse me if this is a duplicate!

Answer 1

It's called an occurrence clause and

The role of an occurrence clause is to select a set of occurrences of a term in a goal.

I'd add "to which the tactic is going to be applied" to the above quote (The Coq Reference manual, sect. 8.1.4).

Then the manual proceeds with the following:

if * is mentioned on the right of |-, the occurrences of the conclusion of the goal have to be selected.

Let's look at some simple cases:

• <tactic> in * |-. applies <tactic> to every hypothesis, but not to the current goal.

• <tactic> in H1, H2 |- *. applies <tactic> only to the hypotheses H1 and H2 and the goal.

• <tactic> in * |- *. applies <tactic> everywhere. There is also a shortcut for this case: <tactic> in *.

For many tactics <tactic> in |- *. is equivalent to just <tactic>. If, for example, you delete all the occurrences of in |- * from the linked file it will still compile.