diff options
| author | Chantal Keller <Chantal.Keller@inria.fr> | 2019-02-08 08:19:51 +0100 |
|---|---|---|
| committer | Valentin Blot <24938579+vblot@users.noreply.github.com> | 2019-02-25 15:33:17 +0100 |
| commit | d5634a96698a29192d292ce03c7e4b7ff42a411a (patch) | |
| tree | fe3baeadc80545caa678821e3e2713f9e03b2b93 /src/Conversion_tactics.v | |
| parent | 10041c91e21dce61faca9725d7073f7c21762019 (diff) | |
| download | smtcoq-d5634a96698a29192d292ce03c7e4b7ff42a411a.tar.gz smtcoq-d5634a96698a29192d292ce03c7e4b7ff42a411a.zip | |
Compile with native-coq
Diffstat (limited to 'src/Conversion_tactics.v')
| -rw-r--r-- | src/Conversion_tactics.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/Conversion_tactics.v b/src/Conversion_tactics.v index d450e3f..37a39b5 100644 --- a/src/Conversion_tactics.v +++ b/src/Conversion_tactics.v @@ -420,7 +420,7 @@ Definition leb : T -> T -> bool := Nat.leb. Lemma t2z_leb_morph : forall x' y', Z.leb (T2Z x') (T2Z y') = leb x' y'. Proof. intros x y; unfold leb. - case_eq (x <=? y); [| rewrite <- 2 Bool.not_true_iff_false]; + case_eq (Nat.leb x y); [| rewrite <- 2 Bool.not_true_iff_false]; rewrite <- Zle_is_le_bool; rewrite Nat.leb_le; rewrite Nat2Z.inj_le; auto. Qed. @@ -428,7 +428,7 @@ Definition ltb : T -> T -> bool := Nat.ltb. Lemma t2z_ltb_morph : forall x' y', Z.ltb (T2Z x') (T2Z y') = ltb x' y'. Proof. intros x y; unfold ltb. - case_eq (x <? y); [| rewrite <- 2 Bool.not_true_iff_false]; + case_eq (Nat.ltb x y); [| rewrite <- 2 Bool.not_true_iff_false]; rewrite <- Zlt_is_lt_bool; rewrite Nat.ltb_lt; rewrite Nat2Z.inj_lt; auto. Qed. @@ -436,7 +436,7 @@ Definition eqb : T -> T -> bool := Nat.eqb. Lemma t2z_eqb_morph : forall x' y', Z.eqb (T2Z x') (T2Z y') = eqb x' y'. Proof. intros x y; unfold eqb. - case_eq (x =? y); [| rewrite <- 2 Bool.not_true_iff_false]; + case_eq (Nat.eqb x y); [| rewrite <- 2 Bool.not_true_iff_false]; rewrite Z.eqb_eq; rewrite Nat.eqb_eq; rewrite Nat2Z.inj_iff; auto. Qed. |