$ coqtop
Welcome to Coq 8.12.2 (January 1980)

Coq < From Coq Require Import Reals.
[Loading ML file newring_plugin.cmxs ... done]
[Loading ML file r_syntax_plugin.cmxs ... done]
[Loading ML file zify_plugin.cmxs ... done]
[Loading ML file micromega_plugin.cmxs ... done]

Coq < From Interval Require Import Plot Tactic.
[Loading ML file interval_plot.cmxs ... done]
[Loading ML file omega_plugin.cmxs ... done]
[Loading ML file ssrmatching_plugin.cmxs ... done]
[Loading ML file ssreflect_plugin.cmxs ... done]
[Loading ML file int63_syntax_plugin.cmxs ... done]
[Loading ML file float_syntax_plugin.cmxs ... done]
[Loading ML file bignums_syntax_plugin.cmxs ... done]

Coq < Open Scope R_scope.

Coq < Definition p1 := ltac:(plot (fun x => x^2 * sin (x^2)) (-4) 4).
p1 is defined

Coq < Plot p1.

Coq < WARNING: Plotting with an 'unknown' terminal.
No output will be generated. Please select a terminal with 'set terminal'.
"/tmp/interval_plotad5922" line 521: undefined variable: mouse