diff options
Diffstat (limited to 'theories/setoid_ring/Ring_polynom.v')
| -rw-r--r-- | theories/setoid_ring/Ring_polynom.v | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/theories/setoid_ring/Ring_polynom.v b/theories/setoid_ring/Ring_polynom.v index e0a3d5a3bf..a13b1fc738 100644 --- a/theories/setoid_ring/Ring_polynom.v +++ b/theories/setoid_ring/Ring_polynom.v @@ -919,14 +919,14 @@ Section MakeRingPol. | PEopp : PExpr -> PExpr | PEpow : PExpr -> N -> PExpr. - Register PExpr as plugins.setoid_ring.pexpr. - Register PEc as plugins.setoid_ring.const. - Register PEX as plugins.setoid_ring.var. - Register PEadd as plugins.setoid_ring.add. - Register PEsub as plugins.setoid_ring.sub. - Register PEmul as plugins.setoid_ring.mul. - Register PEopp as plugins.setoid_ring.opp. - Register PEpow as plugins.setoid_ring.pow. + Register PExpr as plugins.ring.pexpr. + Register PEc as plugins.ring.const. + Register PEX as plugins.ring.var. + Register PEadd as plugins.ring.add. + Register PEsub as plugins.ring.sub. + Register PEmul as plugins.ring.mul. + Register PEopp as plugins.ring.opp. + Register PEpow as plugins.ring.pow. (** evaluation of polynomial expressions towards R *) Definition mk_X j := mkPinj_pred j mkX. |