Я использую протокол XML из Coq 8.6.1. Когда я попробовал вызов PrintAst, мне не удалось получить AST, но вместо этого я получил «todo». Это неисправность или я что-то не так сделал? Как мне получить AST из вызова print AST? Вот мой случай: я...

Определение EvalOp находится в compcert.backend.SplitLongproof : Ltac EvalOp := eauto; match goal with | [ |- eval_exprlist _ _ _ _ _ Enil _ ] => constructor | [ |- eval_exprlist _ _ _ _ _ (_:::_) _ ] => econstructor; EvalOp | [...