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/ZArith/BinIntDef.v | |
| 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/ZArith/BinIntDef.v')
| -rw-r--r-- | theories/ZArith/BinIntDef.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/ZArith/BinIntDef.v b/theories/ZArith/BinIntDef.v index 55b9ec4a44..c05ed9ebf4 100644 --- a/theories/ZArith/BinIntDef.v +++ b/theories/ZArith/BinIntDef.v @@ -208,7 +208,7 @@ Definition gtb x y := | _ => false end. -Fixpoint eqb x y := +Definition eqb x y := match x, y with | 0, 0 => true | pos p, pos q => Pos.eqb p q |