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/NArith | |
| 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/NArith')
| -rw-r--r-- | theories/NArith/BinNatDef.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/NArith/BinNatDef.v b/theories/NArith/BinNatDef.v index ea53618acb..04685cc3eb 100644 --- a/theories/NArith/BinNatDef.v +++ b/theories/NArith/BinNatDef.v @@ -126,7 +126,7 @@ Infix "?=" := compare (at level 70, no associativity) : N_scope. (** Boolean equality and comparison *) -Fixpoint eqb n m := +Definition eqb n m := match n, m with | 0, 0 => true | pos p, pos q => Pos.eqb p q @@ -313,7 +313,7 @@ Definition land n m := (** Logical [diff] *) -Fixpoint ldiff n m := +Definition ldiff n m := match n, m with | 0, _ => 0 | _, 0 => n |