Basically, I want to observe the result of pseudo polynomial division on some instances (say 3 x^2+2 x +1 and 2 x +1). Pseudo division between polynomials is implemented in edivp in polydiv.v in Ssreflect 1.4. I would expect the code should be something like the following:
Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype.
Require Import ssralg poly ssrnum zmodp polydiv interval.
Open Scope Z_scope.
Definition p := Poly [::1;2;3].
Definition q := Poly [:1;2:].
Eval compute in edivp p q.
However, the code stuck at definition p due to a failure in type unification. Any help is greatly appreciated.
I finally had the time to install ssreflect to test your issue. As we discussed in the comments, you should rely on the ssreflect's integer, to get the correct canonical structure instances loaded. Here is my code, using ssr1.4 and coq8.4pl5:
Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype.
Require Import ssralg poly ssrnum zmodp polydiv ssrint.
Open Scope int_scope.
Definition p := Poly [:: 1%:Z;2%:Z;3%:Z].
Definition q := Poly [:: 1%:Z;2%:Z].
Now the Eval compute is correctly typed, but its computation doesn't seem to terminate.
I think this is due to the internal choices of ssr that forbid computations. You should ask more about this directly on ssreflect's mailing list.
Hope this helps, V.