A Maple Mode for Coq. This contribution is an interface between Coq and Maple. In particular, this exports the functions simplify/factor/expand/normal giving the corresponding tactics Simplify/Factor/Expand/Normal. The manipulations carried out by these tactics are proved thanks to the tactic Field. These tactics can be also used as functions by means of the Eval ... In command.
opam install coq-maple-mode.8.5.0