coq - Coq CompCert の EvalOp とは

Question

EvalOp の定義は次のとおりですcompcert.backend.SplitLongproof。

Ltac EvalOp :=
  eauto;
  match goal with
  | [ |- eval_exprlist _ _ _ _ _ Enil _ ] => constructor
  | [ |- eval_exprlist _ _ _ _ _ (_:::_) _ ] => econstructor; EvalOp
  | [ |- eval_expr _ _ _ _ _ (Eletvar _) _ ] => constructor; simpl; eauto
  | [ |- eval_expr _ _ _ _ _ (Elet _ _) _ ] => econstructor; EvalOp
  | [ |- eval_expr _ _ _ _ _ (lift _) _ ] => apply eval_lift; EvalOp
  | [ |- eval_expr _ _ _ _ _ _ _ ] => eapply eval_Eop; [EvalOp | simpl; eauto]
  | _ => idtac
  end.

この定義の奇妙な点は、andを 2 つの別個のトークンとしてcoqdoc --html認識していることです。EvalOp

<span class="id" title="keyword">Eval</span><span class="id" title="var">Op</span>

Coq は、間に区切り文字 (スペース) のない 2 つのトークンを許可するのはなぜですか? それともこれはのバグcoqdocですか？助けてくれてありがとう！