diff options
Diffstat (limited to 'theories/MSets/MSetRBT.v')
| -rw-r--r-- | theories/MSets/MSetRBT.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/MSets/MSetRBT.v b/theories/MSets/MSetRBT.v index b53c03920..35d8245a7 100644 --- a/theories/MSets/MSetRBT.v +++ b/theories/MSets/MSetRBT.v @@ -282,7 +282,7 @@ Fixpoint treeify_aux (pred:bool)(n: positive) : treeify_t := Fixpoint plength (l:list elt) := match l with | nil => 1%positive - | _::l => Psucc (plength l) + | _::l => Pos.succ (plength l) end. Definition treeify (l:list elt) := |