Closed brando90 closed 2 years ago
See the argument for TacArg:
https://github.com/ejgallego/coq-serapi/blob/b222c1f821694175273d3a295a04abf9454f6727/serlib/plugins/ltac/ser_tacexpr.ml#L232
but the reply has a type CAst.t as an argument for TacArg:
(Parse () "(___hole O).") (Answer 24 Ack) (Answer 24 (ObjList ((CoqAst ((v ((control ()) (attrs ()) (expr (VernacExtend (VernacSolve 0) ((GenArg raw (OptArg (ExtraArg ltac_selector)) ()) (GenArg raw (OptArg (ExtraArg ltac_info)) ()) (GenArg raw (ExtraArg tactic) (TacArg ((v (TacCall ((v (((v (Ser_Qualid (DirPath ()) (Id ___hole))) (loc (((fname ToplevelInput) (line_nb 1) (bol_pos 0) (line_nb_last 1) (bol_pos_last 0) (bp 1) (ep 8))))) ((Reference ((v (Ser_Qualid (DirPath ()) (Id O))) (loc (((fname ToplevelInput) (line_nb 1) (bol_pos 0) (line_nb_last 1) (bol_pos_last 0) (bp 9) (ep 10))))))))) (loc (((fname ToplevelInput) (line_nb 1) (bol_pos 0) (line_nb_last 1) (bol_pos_last 0) (bp 1) (ep 10))))))) (loc (((fname ToplevelInput) (line_nb 1) (bol_pos 0) (line_nb_last 1) (bol_pos_last 0) (bp 1) (ep 10))))))) (GenArg raw (ExtraArg ltac_use_default) false)))))) (loc (((fname ToplevelInput) (line_nb 1) (bol_pos 0) (line_nb_last 1) (bol_pos_last 0) (bp 0) (ep 12))))))))) (Answer 24 Completed
doesn't make sense to me. Why?
In addition if I send it some TacArg with value CAst.t it parses it correctly but I think it shouldn't:
(Print ((sid 6) (pp ((pp_format PpStr)))) (CoqGenArg (GenArg raw (ExtraArg tactic) (TacArg ((v (Reference ((v (Ser_Qualid (DirPath ()) (Id O))) (loc (((fname ToplevelInput) (line_nb 1) (bol_pos 0) (line_nb_last 1) (bol_pos_last 0) (bp 9) (ep 10))))))) (loc (((fname ToplevelInput) (line_nb 1) (bol_pos 0) (line_nb_last 1) (bol_pos_last 0) (bp 1) (ep 10))))))) ) ) (Answer 23 Ack) (Answer 23 (ObjList ((CoqString O)))) (Answer 23 Completed)
cross: https://proofassistants.stackexchange.com/questions/1604/why-does-tacarg-accepts-a-value-of-cast-t-type-when-it-should-only-accept-values
The input type here is gen_tactic_expr, not gen_tactic_expr_r which is the one you are pointing out to.
gen_tactic_expr
gen_tactic_expr_r
I think this answers the question.
See the argument for TacArg:
https://github.com/ejgallego/coq-serapi/blob/b222c1f821694175273d3a295a04abf9454f6727/serlib/plugins/ltac/ser_tacexpr.ml#L232
but the reply has a type CAst.t as an argument for TacArg:
doesn't make sense to me. Why?
In addition if I send it some TacArg with value CAst.t it parses it correctly but I think it shouldn't:
cross: https://proofassistants.stackexchange.com/questions/1604/why-does-tacarg-accepts-a-value-of-cast-t-type-when-it-should-only-accept-values