diff options
| author | Pierre-Marie Pédrot | 2018-12-20 14:57:17 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-12-20 14:57:17 +0100 |
| commit | 8d41928c9f0bb54ed41e3ab0d7a6f76d556bb588 (patch) | |
| tree | 80cacb02f1e8785c30ce2fd7fe662a5efa1c2cba /plugins/setoid_ring/Ring_polynom.v | |
| parent | 525d174b6e6f966e95b3c1f649c8b83ef52abd75 (diff) | |
| parent | 0a25e351d6a2d25e5d82b165843a09a2804fadc6 (diff) | |
Merge PR #8488: Warning when using automatic template polymorphism
Diffstat (limited to 'plugins/setoid_ring/Ring_polynom.v')
| -rw-r--r-- | plugins/setoid_ring/Ring_polynom.v | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/plugins/setoid_ring/Ring_polynom.v b/plugins/setoid_ring/Ring_polynom.v index ccd82eabcd..9ef24144d2 100644 --- a/plugins/setoid_ring/Ring_polynom.v +++ b/plugins/setoid_ring/Ring_polynom.v @@ -121,6 +121,7 @@ Section MakeRingPol. - (Pinj i (Pc c)) is (Pc c) *) + #[universes(template)] Inductive Pol : Type := | Pc : C -> Pol | Pinj : positive -> Pol -> Pol @@ -908,6 +909,7 @@ Section MakeRingPol. (** Definition of polynomial expressions *) + #[universes(template)] Inductive PExpr : Type := | PEO : PExpr | PEI : PExpr |