diff options
| author | Hugo Herbelin | 2020-04-19 13:00:09 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-05-01 23:17:27 +0200 |
| commit | df8df4637dfb4106854554cc2ac94b4fdd565e80 (patch) | |
| tree | 8bedbb603f032642d8bf1c553121ae091077f692 /theories/FSets | |
| parent | a6b2029042ae2e5f51fcae6d922fc8437ae1ff13 (diff) | |
Fixing #11903: Fixpoints not truly recursive in standard library.
There was also a non truly recursive in the doc.
Diffstat (limited to 'theories/FSets')
| -rw-r--r-- | theories/FSets/FMapAVL.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/FSets/FMapAVL.v b/theories/FSets/FMapAVL.v index f78c0ecc1e..ad0124db6d 100644 --- a/theories/FSets/FMapAVL.v +++ b/theories/FSets/FMapAVL.v @@ -123,7 +123,7 @@ Definition create l x e r := Definition assert_false := create. -Fixpoint bal l x d r := +Definition bal l x d r := let hl := height l in let hr := height r in if gt_le_dec hl (hr+2) then @@ -191,7 +191,7 @@ Fixpoint remove_min l x d r : t*(key*elt) := [|height t1 - height t2| <= 2]. *) -Fixpoint merge s1 s2 := match s1,s2 with +Definition merge s1 s2 := match s1,s2 with | Leaf, _ => s2 | _, Leaf => s1 | _, Node l2 x2 d2 r2 h2 => |