diff options
Diffstat (limited to 'plugins/setoid_ring/Ncring_polynom.v')
| -rw-r--r-- | plugins/setoid_ring/Ncring_polynom.v | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/plugins/setoid_ring/Ncring_polynom.v b/plugins/setoid_ring/Ncring_polynom.v index 6a8c514a7b..048c8eecf9 100644 --- a/plugins/setoid_ring/Ncring_polynom.v +++ b/plugins/setoid_ring/Ncring_polynom.v @@ -32,7 +32,6 @@ Variable phiCR_comm: forall (c:C)(x:R), x * [c] == [c] * x. with coefficients in C : *) -#[universes(template)] Inductive Pol : Type := | Pc : C -> Pol | PX : Pol -> positive -> positive -> Pol -> Pol. |