Why does TacArg accepts a value of CAst.t type when it should only accept values of types

[brando90]

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

[ejgallego]

The input type here is gen_tactic_expr, not gen_tactic_expr_r which is the one you are pointing out to.

[ejgallego]

I think this answers the question.