Что делают фигурные скобки {} в ssreflect rewrite

Question

Я читаю и играю с учебником ssreflect и столкнулся с использованием {} для цитирования вещей, которые я не совсем понимаю:

Variables P Q : bool -> Prop.
Hypothesis P2Q : forall a b, P (a || b) -> Q a.
Goal forall a, P (a || a) -> True.
  move=> a HPa. move: {HPa} (@P2Q _ _ HPa) => HQa.

Может кто-нибудь объяснить, что делает {HPa} сделать для HPa?

Кстати, контекст должен был ввести "взгляды". Я пытался удалить {}, он все еще работает, но генерирует что-то другое. И я не знаю, где искать документацию для таких вещей, как скобки или @ в этом отношении.

Answer 1

После некоторых экспериментов и сравнения, кажется, что функция {H} это к clear H. в терминах Coq.

move: {HPa} (@P2Q _ _ HPa) => HQa.

дает

1 subgoals
a : bool
HQa : Q a
______________________________________(1/1)
True

в то время как

move: (@P2Q _ _ HPa) => HQa.

дает то же самое, за исключением того, что HPa сохраняется без изменений в контексте:

1 subgoals
a : bool
HPa : P (a || a)
HQa : Q a
______________________________________(1/1)
True