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!
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.