Refinement of mpoly with the Pol structure from micromega#107

Open

proux01 wants to merge 3 commits into

Annotations

1 error and 10 warnings

Cannot find a physical path bound to logical path

Notation ringType is deprecated since mathcomp 2.4.0.

Notation ringType is deprecated since mathcomp 2.4.0.

Notation ringType is deprecated since mathcomp 2.4.0.

Notation ringType is deprecated since mathcomp 2.4.0.

Notations "[ f set _ | _ in _ ]" defined at level 0 with arguments

Notations "[ fset[ _ ] _ | _ : _ in _ ]" defined at level 0

Notations "[ fset[ _ ] _ | _ in _ ]" defined at level 0

Notations "[ fset[ _ ] _ | _ : _ in _ ]" defined at level 0

Notations "[ fset _ | _ in _ ]" defined at level 0 with arguments

Notations "[ fset _ | _ : _ in _ ]" defined at level 0