Compare revisions

9274984b · 9274984b · 9274984b · 9274984b · 9274984b · 9274984b
--- a/theories/list.v
+++ b/theories/list.v
--- a/stdpp/list_tactics.v
+++ b/stdpp/list_tactics.v
--- a/theories/listset.v
+++ b/theories/listset.v
@@ -28,7 +28,7 @@ Lemma listset_empty_alt X : X ≡ ∅ ↔ listset_car X = [].
 Proof.
  destruct X as [l]; split; [|by intros; simplify_eq/=].
  rewrite elem_of_equiv_empty; intros Hl.
-  destruct l as [|x l]; [done|]. feed inversion (Hl x). left.
+  destruct l as [|x l]; [done|]. oinversion Hl. left.
 Qed.
 Global Instance listset_empty_dec (X : listset A) : Decision (X ≡ ∅).
 Proof.

--- a/theories/listset_nodup.v
+++ b/theories/listset_nodup.v
--- a/theories/mapset.v
+++ b/theories/mapset.v
--- a/theories/namespaces.v
+++ b/theories/namespaces.v
--- a/theories/nat_cancel.v
+++ b/theories/nat_cancel.v
--- a/theories/natmap.v
+++ b/theories/natmap.v
--- a/theories/nmap.v
+++ b/theories/nmap.v
--- a/stdpp/numbers.v
+++ b/stdpp/numbers.v
--- a/theories/option.v
+++ b/theories/option.v
--- a/theories/options.v
+++ b/theories/options.v
--- a/theories/orders.v
+++ b/theories/orders.v
--- a/stdpp/pmap.v
+++ b/stdpp/pmap.v
--- a/theories/prelude.v
+++ b/theories/prelude.v
--- a/theories/pretty.v
+++ b/theories/pretty.v
@@ -113,7 +113,7 @@ Proof. apply _. Qed.
 Global Instance pretty_Z : Pretty Z := λ x,
  match x with
  | Z0 => "0" | Zpos x => pretty x | Zneg x => "-" +:+ pretty x
-  end%string.
+  end.
 Global Instance pretty_Z_inj : Inj (=@{Z}) (=) pretty.
 Proof.
  unfold pretty, pretty_Z.

--- a/theories/proof_irrel.v
+++ b/theories/proof_irrel.v
--- a/theories/propset.v
+++ b/theories/propset.v
--- a/theories/relations.v
+++ b/theories/relations.v
--- a/theories/sets.v
+++ b/theories/sets.v
No results found