Questions tagged [coq-serapi]
The coq-serapi tag has no usage guidance.
3
questions
1
vote
0
answers
22
views
Why does TacArg accepts a value of CAst.t type when it should only accept values of types?
See the argument for TacArg:
| TacArg of ('t, 'dtrm, 'p, 'c, 'r, 'n, 'tacexpr, 'l) gen_tactic_arg
but the reply has a type CAst.t as an argument for TacArg:
<...
- 169
5
votes
0
answers
56
views
What are Generic Arguments in Coq and how are they structured in their OCaml code?
I was trying to figure out why it seems that in a Coq generic argument there seems to be 3 arguments to the constructor GenArg when according to me there should ...
- 169
5
votes
0
answers
132
views
How does one systematically traverse OCaml representations of Coq ASTs terms?
I want to be able to (tree) traverse Coq terms (e.g. in OCaml or using their s-expression representation in any language).
My main challenge is to figure out how to do this systematically because I ...
- 169