Hello,

We develop an OCaml code to automate repetitive calculations and to 
assemble proofs in the mathematical domain of PDE homogenization (to 
summarize in one sentence).

We now need to embed elementary symbolic calculations.

Do you know a library of "Computer Algebra" which interfaces well with 
OCaml?
Does COQ need symbolic calculus? If so, is there a core of CA in COQ?

Thank you for your help,
Nicolas