What is the EvalOp in Coq CompCert

Question

The definition of EvalOp is in 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.

What is strange about this definition is that coqdoc --html recognize Eval and Op as two separate tokens:

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

Why would Coq allow two tokens with no separators (spaces) in the middle? Or is this a bug of coqdoc? Thanks for helping!

Answer 1

Why would Coq allow two tokens with no separators (spaces) in the middle? Or is this a bug of coqdoc?

This is a bug of coqdoc. Coq does not allow two alphabetic tokens with no non-alphanumeric characters between them, but there are plenty of other examples of tokens without separators. For example, this is valid Coq:

Definition(*no-spaces*)foo:=1.

This gets lexed as the tokens Definition, the comment (*no-spaces*), foo, :=, 1, and ., I believe. You can also play silly games with numeric tokens, e.g.,

Coercion Nat.add:nat>->Funclass.
Axiom a:nat.
Check 1a:nat.

Because identifiers cannot start with numbers, Coq parses 1a as 1 applied to a, which typechecks because of the Coercion. You should probably not play games like this with Coq's parser.