diff options
| author | Jasper Hugunin | 2020-09-12 18:01:56 -0700 |
|---|---|---|
| committer | Jasper Hugunin | 2020-09-16 12:46:57 -0700 |
| commit | 9daa2ec464eb9b881cab7d53fd39efc5de3afe12 (patch) | |
| tree | 92c08a69abe93a13b4f1d3c55f770fe1bb9f1731 | |
| parent | aa9f22f930a2207d5ff8e9ab88ddb08288245eee (diff) | |
Modify NArith/Nnat.v to compile with -mangle-names
| -rw-r--r-- | theories/NArith/Nnat.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/theories/NArith/Nnat.v b/theories/NArith/Nnat.v index 43fa8516d3..48df5fe884 100644 --- a/theories/NArith/Nnat.v +++ b/theories/NArith/Nnat.v @@ -70,7 +70,7 @@ Lemma inj_sub a a' : N.to_nat (a - a') = N.to_nat a - N.to_nat a'. Proof. destruct a as [|a], a' as [|a']; simpl; rewrite ?Nat.sub_0_r; trivial. - destruct (Pos.compare_spec a a'). + destruct (Pos.compare_spec a a') as [H|H|H]. - subst. now rewrite Pos.sub_mask_diag, Nat.sub_diag. - rewrite Pos.sub_mask_neg; trivial. apply Pos2Nat.inj_lt in H. simpl; symmetry; apply Nat.sub_0_le. now apply Nat.lt_le_incl. @@ -93,8 +93,8 @@ Qed. Lemma inj_compare a a' : (a ?= a')%N = (N.to_nat a ?= N.to_nat a'). Proof. - destruct a, a'; simpl; trivial. - - now destruct (Pos2Nat.is_succ p) as (n,->). + destruct a as [|p], a' as [|p']; simpl; trivial. + - now destruct (Pos2Nat.is_succ p') as (n,->). - now destruct (Pos2Nat.is_succ p) as (n,->). - apply Pos2Nat.inj_compare. Qed. |