diff options
| author | Jasper Hugunin | 2020-09-12 21:03:31 -0700 |
|---|---|---|
| committer | Jasper Hugunin | 2020-09-16 13:23:13 -0700 |
| commit | cc4494897f0897f5795c2bd25fc06d4b07c73667 (patch) | |
| tree | 596ed5ed585ee2cf9acf6ba2a8af26faa7a0d5ba /theories/setoid_ring | |
| parent | 862a5b352e784fff9f1a9bde5ac3b887403ece57 (diff) | |
Modify setoid_ring/BinList.v to compile with -mangle-names
Diffstat (limited to 'theories/setoid_ring')
| -rw-r--r-- | theories/setoid_ring/BinList.v | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/theories/setoid_ring/BinList.v b/theories/setoid_ring/BinList.v index b6b8b45e1a..892909fd40 100644 --- a/theories/setoid_ring/BinList.v +++ b/theories/setoid_ring/BinList.v @@ -33,13 +33,13 @@ Section MakeBinList. Lemma jump_tl : forall j l, tl (jump j l) = jump j (tl l). Proof. - induction j;simpl;intros; now rewrite ?IHj. + intro j;induction j as [j IHj|j IHj|];simpl;intros; now rewrite ?IHj. Qed. Lemma jump_succ : forall j l, jump (Pos.succ j) l = jump 1 (jump j l). Proof. - induction j;simpl;intros. + intro j;induction j as [j IHj|j IHj|];simpl;intros. - rewrite !IHj; simpl; now rewrite !jump_tl. - now rewrite !jump_tl. - trivial. @@ -48,7 +48,7 @@ Section MakeBinList. Lemma jump_add : forall i j l, jump (i + j) l = jump i (jump j l). Proof. - induction i using Pos.peano_ind; intros. + intro i; induction i as [|i IHi] using Pos.peano_ind; intros. - now rewrite Pos.add_1_l, jump_succ. - now rewrite Pos.add_succ_l, !jump_succ, IHi. Qed. @@ -56,7 +56,7 @@ Section MakeBinList. Lemma jump_pred_double : forall i l, jump (Pos.pred_double i) (tl l) = jump i (jump i l). Proof. - induction i;intros;simpl. + intro i;induction i as [i IHi|i IHi|];intros;simpl. - now rewrite !jump_tl. - now rewrite IHi, <- 2 jump_tl, IHi. - trivial. @@ -64,7 +64,7 @@ Section MakeBinList. Lemma nth_jump : forall p l, nth p (tl l) = hd default (jump p l). Proof. - induction p;simpl;intros. + intro p;induction p as [p IHp|p IHp|];simpl;intros. - now rewrite <-jump_tl, IHp. - now rewrite <-jump_tl, IHp. - trivial. @@ -73,7 +73,7 @@ Section MakeBinList. Lemma nth_pred_double : forall p l, nth (Pos.pred_double p) (tl l) = nth p (jump p l). Proof. - induction p;simpl;intros. + intro p;induction p as [p IHp|p IHp|];simpl;intros. - now rewrite !jump_tl. - now rewrite jump_pred_double, <- !jump_tl, IHp. - trivial. |