Commit e2efc09c authored by Ralf Jung's avatar Ralf Jung

Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coq

parents 6ca92264 eb563833
......@@ -272,8 +272,12 @@ Lemma cmra_unit_preserving x y : x ≼ y → unit x ≼ unit y.
Proof. rewrite !cmra_included_includedN; eauto using cmra_unit_preservingN. Qed.
Lemma cmra_included_unit x : unit x x.
Proof. by exists x; rewrite cmra_unit_l. Qed.
Lemma cmra_preservingN_l n x y z : x {n} y z x {n} z y.
Proof. by intros [z1 Hz1]; exists z1; rewrite Hz1 (associative op). Qed.
Lemma cmra_preserving_l x y z : x y z x z y.
Proof. by intros [z1 Hz1]; exists z1; rewrite Hz1 (associative op). Qed.
Lemma cmra_preservingN_r n x y z : x {n} y x z {n} y z.
Proof. by intros; rewrite -!(commutative _ z); apply cmra_preservingN_l. Qed.
Lemma cmra_preserving_r x y z : x y x z y z.
Proof. by intros; rewrite -!(commutative _ z); apply cmra_preserving_l. Qed.
......
......@@ -28,10 +28,6 @@ Notation "x ≤ y ≤ z ≤ z'" := (x ≤ y ∧ y ≤ z ∧ z ≤ z')%nat : nat_
Notation "(≤)" := le (only parsing) : nat_scope.
Notation "(<)" := lt (only parsing) : nat_scope.
Infix "≥" := ge : nat_scope.
Notation "(≥)" := ge (only parsing) : nat_scope.
Notation "(>)" := gt (only parsing) : nat_scope.
Infix "`div`" := Nat.div (at level 35) : nat_scope.
Infix "`mod`" := Nat.modulo (at level 35) : nat_scope.
......@@ -108,10 +104,6 @@ Notation "(<)" := Pos.lt (only parsing) : positive_scope.
Notation "(~0)" := xO (only parsing) : positive_scope.
Notation "(~1)" := xI (only parsing) : positive_scope.
Infix "≥" := Pos.ge : positive_scope.
Notation "(≥)" := Pos.ge (only parsing) : positive_scope.
Notation "(>)" := Pos.gt (only parsing) : positive_scope.
Arguments Pos.of_nat _ : simpl never.
Instance positive_eq_dec: x y : positive, Decision (x = y) := Pos.eq_dec.
Instance positive_inhabited: Inhabited positive := populate 1.
......@@ -187,11 +179,6 @@ Notation "x < y ≤ z" := (x < y ∧ y ≤ z)%N : N_scope.
Notation "x ≤ y ≤ z ≤ z'" := (x y y z z z')%N : N_scope.
Notation "(≤)" := N.le (only parsing) : N_scope.
Notation "(<)" := N.lt (only parsing) : N_scope.
Infix "≥" := N.ge : N_scope.
Notation "(≥)" := N.ge (only parsing) : N_scope.
Notation "(>)" := N.gt (only parsing) : N_scope.
Infix "`div`" := N.div (at level 35) : N_scope.
Infix "`mod`" := N.modulo (at level 35) : N_scope.
......@@ -226,10 +213,6 @@ Notation "x ≤ y ≤ z ≤ z'" := (x ≤ y ∧ y ≤ z ∧ z ≤ z') : Z_scope.
Notation "(≤)" := Z.le (only parsing) : Z_scope.
Notation "(<)" := Z.lt (only parsing) : Z_scope.
Infix "≥" := Z.ge : Z_scope.
Notation "(≥)" := Z.ge (only parsing) : Z_scope.
Notation "(>)" := Z.gt (only parsing) : Z_scope.
Infix "`div`" := Z.div (at level 35) : Z_scope.
Infix "`mod`" := Z.modulo (at level 35) : Z_scope.
Infix "`quot`" := Z.quot (at level 35) : Z_scope.
......@@ -345,10 +328,6 @@ Notation "x ≤ y ≤ z ≤ z'" := (x ≤ y ∧ y ≤ z ∧ z ≤ z') : Qc_scope
Notation "(≤)" := Qcle (only parsing) : Qc_scope.
Notation "(<)" := Qclt (only parsing) : Qc_scope.
Infix "≥" := Qcge : Qc_scope.
Notation "(≥)" := Qcge (only parsing) : Qc_scope.
Notation "(>)" := Qcgt (only parsing) : Qc_scope.
Hint Extern 1 (_ _) => reflexivity || discriminate.
Arguments Qred _ : simpl never.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment