From 02f213ce883755c487150fcd89cededc8ea7e8c8 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 7 Oct 2015 13:13:11 +0200
Subject: [PATCH] Port to Coq 8.5 beta 2.

The port makes the following notable changes:

* The carrier types of separation algebras and integer environments are no
  longer in Set. Now they have a type at a fixed type level above Set. This
  both works better in 8.5 and makes the formalization more general.
  I have tried putting them at polymorphic type levels, but that increased the
  compilation time by an order of magnitude.
* I am using a custom f_equal tactic written in Ltac to circumvent bug #4069.
  That bug has been fixed, so this custom tactic can be removed when the next
  beta of 8.5 is out.
---
 theories/assoc.v       |  2 +-
 theories/base.v        | 17 ++++++------
 theories/collections.v |  3 +--
 theories/countable.v   |  6 ++---
 theories/decidable.v   |  6 +----
 theories/error.v       |  2 +-
 theories/list.v        | 16 +++++------
 theories/mapset.v      | 39 +++++++++++++--------------
 theories/natmap.v      |  2 +-
 theories/nmap.v        |  4 +--
 theories/numbers.v     |  4 +--
 theories/optionmap.v   |  3 +--
 theories/orders.v      |  2 +-
 theories/pmap.v        | 10 +++----
 theories/pretty.v      | 60 ++++++++++++++++++++++++++----------------
 theories/stringmap.v   |  2 +-
 theories/tactics.v     | 13 +++++++++
 theories/zmap.v        |  4 +--
 18 files changed, 108 insertions(+), 87 deletions(-)

diff --git a/theories/assoc.v b/theories/assoc.v
index 37b6c816..c9e609ba 100644
--- a/theories/assoc.v
+++ b/theories/assoc.v
@@ -269,7 +269,7 @@ End assoc.
 
 (** * Finite sets *)
 (** We construct finite sets using the above implementation of maps. *)
-Notation assoc_set K := (mapset (assoc K unit)).
+Notation assoc_set K := (mapset (assoc K)).
 Instance assoc_map_dom `{Lexico K, !TrichotomyT (@lexico K _),
   !StrictOrder lexico} {A} : Dom (assoc K A) (assoc_set K) := mapset_dom.
 Instance assoc_map_dom_spec `{Lexico K} `{!TrichotomyT (@lexico K _)}
diff --git a/theories/base.v b/theories/base.v
index 24ea3864..4823508f 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -6,6 +6,7 @@ abstract interfaces for ordered structures, collections, and various other data
 structures. *)
 Global Generalizable All Variables.
 Global Set Automatic Coercions Import.
+Global Set Asymmetric Patterns.
 Require Export Morphisms RelationClasses List Bool Utf8 Program Setoid.
 
 (** * General *)
@@ -418,23 +419,23 @@ Notation "(≫= f )" := (mbind f) (only parsing) : C_scope.
 Notation "(≫=)" := (λ m f, mbind f m) (only parsing) : C_scope.
 
 Notation "x ← y ; z" := (y ≫= (λ x : _, z))
-  (at level 65, next at level 35, only parsing, right associativity) : C_scope.
+  (at level 65, only parsing, right associativity) : C_scope.
 Infix "<$>" := fmap (at level 60, right associativity) : C_scope.
 Notation "' ( x1 , x2 ) ← y ; z" :=
   (y ≫= (λ x : _, let ' (x1, x2) := x in z))
-  (at level 65, next at level 35, only parsing, right associativity) : C_scope.
+  (at level 65, only parsing, right associativity) : C_scope.
 Notation "' ( x1 , x2 , x3 ) ← y ; z" :=
   (y ≫= (λ x : _, let ' (x1,x2,x3) := x in z))
-  (at level 65, next at level 35, only parsing, right associativity) : C_scope.
+  (at level 65, only parsing, right associativity) : C_scope.
 Notation "' ( x1 , x2 , x3  , x4 ) ← y ; z" :=
   (y ≫= (λ x : _, let ' (x1,x2,x3,x4) := x in z))
-  (at level 65, next at level 35, only parsing, right associativity) : C_scope.
+  (at level 65, only parsing, right associativity) : C_scope.
 Notation "' ( x1 , x2 , x3  , x4 , x5 ) ← y ; z" :=
   (y ≫= (λ x : _, let ' (x1,x2,x3,x4,x5) := x in z))
-  (at level 65, next at level 35, only parsing, right associativity) : C_scope.
+  (at level 65, only parsing, right associativity) : C_scope.
 Notation "' ( x1 , x2 , x3  , x4 , x5 , x6 ) ← y ; z" :=
   (y ≫= (λ x : _, let ' (x1,x2,x3,x4,x5,x6) := x in z))
-  (at level 65, next at level 35, only parsing, right associativity) : C_scope.
+  (at level 65, only parsing, right associativity) : C_scope.
 
 Notation "ps .*1" := (fmap (M:=list) fst ps)
   (at level 10, format "ps .*1").
@@ -445,9 +446,9 @@ Class MGuard (M : Type → Type) :=
   mguard: ∀ P {dec : Decision P} {A}, (P → M A) → M A.
 Arguments mguard _ _ _ !_ _ _ /.
 Notation "'guard' P ; o" := (mguard P (λ _, o))
-  (at level 65, next at level 35, only parsing, right associativity) : C_scope.
+  (at level 65, only parsing, right associativity) : C_scope.
 Notation "'guard' P 'as' H ; o" := (mguard P (λ H, o))
-  (at level 65, next at level 35, only parsing, right associativity) : C_scope.
+  (at level 65, only parsing, right associativity) : C_scope.
 
 (** ** Operations on maps *)
 (** In this section we define operational type classes for the operations
diff --git a/theories/collections.v b/theories/collections.v
index 825d4664..281f7ef3 100644
--- a/theories/collections.v
+++ b/theories/collections.v
@@ -109,8 +109,7 @@ Section of_option_list.
   Proof.
     split.
     * induction l; simpl; [by rewrite elem_of_empty|].
-      rewrite elem_of_union, elem_of_singleton;
-        intros [->|?]; constructor (auto).
+      rewrite elem_of_union,elem_of_singleton; intros [->|?]; constructor; auto.
     * induction 1; simpl; rewrite elem_of_union, elem_of_singleton; auto.
   Qed.
 End of_option_list.
diff --git a/theories/countable.v b/theories/countable.v
index 42095618..c62eb235 100644
--- a/theories/countable.v
+++ b/theories/countable.v
@@ -68,7 +68,7 @@ Lemma surjective_cancel `{Countable A} `{∀ x y : B, Decision (x = y)}
   (f : A → B) `{!Surjective (=) f} : { g : B → A & Cancel (=) f g }.
 Proof.
   exists (λ y, choose (λ x, f x = y) (surjective f y)).
-  intros y. by rewrite (choose_correct (λ _, _) (surjective f y)).
+  intros y. by rewrite (choose_correct (λ x, f x = y) (surjective f y)).
 Qed.
 
 (** ** Instances *)
@@ -200,7 +200,7 @@ Program Instance list_countable `{Countable A} : Countable (list A) :=  {|
   decode p := list_decode p ≫= mapM decode
 |}.
 Next Obligation.
-  intros ??? l. rewrite list_decode_encode. simpl.
+  intros ??? l; simpl; rewrite list_decode_encode; simpl.
   apply mapM_fmap_Some; auto using decode_encode.
 Qed.
 
@@ -227,5 +227,5 @@ Program Instance nat_countable : Countable nat := {|
   decode p := N.to_nat <$> decode p
 |}.
 Next Obligation.
-  intros x. rewrite decode_encode; csimpl. by rewrite Nat2N.id.
+  intros x; lazy beta; rewrite decode_encode; csimpl. by rewrite Nat2N.id.
 Qed.
diff --git a/theories/decidable.v b/theories/decidable.v
index 7adf535d..96720b24 100644
--- a/theories/decidable.v
+++ b/theories/decidable.v
@@ -125,13 +125,9 @@ Proof. repeat case_bool_decide; tauto. Qed.
 (** Leibniz equality on Sigma types requires the equipped proofs to be
 equal as Coq does not support proof irrelevance. For decidable we
 propositions we define the type [dsig P] whose Leibniz equality is proof
-irrelevant. That is [∀ x y : dsig P, x = y ↔ `x = `y]. Due to the absence of
-universe polymorpic definitions we also define a variant [dsigS] for types
-in [Set]. *)
+irrelevant. That is [∀ x y : dsig P, x = y ↔ `x = `y]. *)
 Definition dsig `(P : A → Prop) `{∀ x : A, Decision (P x)} :=
   { x | bool_decide (P x) }.
-Definition dsigS {A : Set} (P : A → Prop) `{∀ x : A, Decision (P x)} : Set :=
-  { x | bool_decide (P x) }.
 
 Definition proj2_dsig `{∀ x : A, Decision (P x)} (x : dsig P) : P (`x) :=
   bool_decide_unpack _ (proj2_sig x).
diff --git a/theories/error.v b/theories/error.v
index 1cef6fff..46fe0c57 100644
--- a/theories/error.v
+++ b/theories/error.v
@@ -27,7 +27,7 @@ Definition error_guard {E} P {dec : Decision P} {S A}
     (e : E) (f : P → error S E A) : error S E A :=
   match decide P with left H => f H | right _ => fail e end.
 Notation "'guard' P 'with' e ; o" := (error_guard P e (λ _, o))
-  (at level 65, next at level 35, only parsing, right associativity) : C_scope.
+  (at level 65, only parsing, right associativity) : C_scope.
 Definition error_of_option {S A E} (x : option A) (e : E) : error S E A :=
   match x with Some a => mret a | None => fail e end.
 
diff --git a/theories/list.v b/theories/list.v
index 403ac4e4..89f7a0a9 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -586,7 +586,7 @@ Proof. destruct l. done. by edestruct 1; constructor. Qed.
 Lemma elem_of_not_nil x l : x ∈ l → l ≠ [].
 Proof. intros ? ->. by apply (elem_of_nil x). Qed.
 Lemma elem_of_cons l x y : x ∈ y :: l ↔ x = y ∨ x ∈ l.
-Proof. split; [inversion 1; subst|intros [->|?]]; constructor (done). Qed.
+Proof. by split; [inversion 1; subst|intros [->|?]]; constructor. Qed.
 Lemma not_elem_of_cons l x y : x ∉ y :: l ↔ x ≠ y ∧ x ∉ l.
 Proof. rewrite elem_of_cons. tauto. Qed.
 Lemma elem_of_app l1 l2 x : x ∈ l1 ++ l2 ↔ x ∈ l1 ∨ x ∈ l2.
@@ -623,8 +623,8 @@ Proof.
   split.
   * induction l as [|x l]; csimpl; repeat case_match; inversion 1; subst;
       setoid_rewrite elem_of_cons; naive_solver.
-  * intros (x&Hx&?). induction Hx; csimpl; repeat case_match;
-      simplify_equality; auto; constructor (by auto).
+  * intros (x&Hx&?). by induction Hx; csimpl; repeat case_match;
+      simplify_equality; try constructor; auto.
 Qed.
 
 (** ** Properties of the [NoDup] predicate *)
@@ -1311,7 +1311,7 @@ Definition Permutation_skip := @perm_skip A.
 Definition Permutation_swap := @perm_swap A.
 Definition Permutation_singleton_inj := @Permutation_length_1 A.
 
-Global Existing Instance Permutation_app'_Proper.
+Global Existing Instance Permutation_app'.
 Global Instance: Proper ((≡ₚ) ==> (=)) (@length A).
 Proof. induction 1; simpl; auto with lia. Qed.
 Global Instance: Commutative (≡ₚ) (@app A).
@@ -2037,7 +2037,7 @@ Section Forall_Exists.
   Proof. intros H ?. induction H; auto. Defined.
   Global Instance Forall_proper:
     Proper (pointwise_relation _ (↔) ==> (=) ==> (↔)) (@Forall A).
-  Proof. split; subst; induction 1; constructor (by firstorder auto). Qed.
+  Proof. split; subst; induction 1; constructor; by firstorder auto. Qed.
   Lemma Forall_iff l (Q : A → Prop) :
     (∀ x, P x ↔ Q x) → Forall P l ↔ Forall Q l.
   Proof. intros H. apply Forall_proper. red; apply H. done. Qed.
@@ -2150,7 +2150,7 @@ Section Forall_Exists.
   Proof. intros H ?. induction H; auto. Defined.
   Global Instance Exists_proper:
     Proper (pointwise_relation _ (↔) ==> (=) ==> (↔)) (@Exists A).
-  Proof. split; subst; induction 1; constructor (by firstorder auto). Qed.
+  Proof. split; subst; induction 1; constructor; by firstorder auto. Qed.
   Lemma Exists_not_Forall l : Exists (not ∘ P) l → ¬Forall P l.
   Proof. induction 1; inversion_clear 1; contradiction. Qed.
   Lemma Forall_not_Exists l : Forall (not ∘ P) l → ¬Exists P l.
@@ -2466,7 +2466,7 @@ Section Forall2_order.
   Global Instance: Symmetric R → Symmetric (Forall2 R).
   Proof. intros. induction 1; constructor; auto. Qed.
   Global Instance: Transitive R → Transitive (Forall2 R).
-  Proof. intros ????. apply Forall2_transitive. apply transitivity. Qed.
+  Proof. intros ????. apply Forall2_transitive. by apply @transitivity. Qed.
   Global Instance: Equivalence R → Equivalence (Forall2 R).
   Proof. split; apply _. Qed.
   Global Instance: PreOrder R → PreOrder (Forall2 R).
@@ -2658,7 +2658,7 @@ Section fmap.
   Lemma Forall_fmap (P : B → Prop) l : Forall P (f <$> l) ↔ Forall (P ∘ f) l.
   Proof. split; induction l; inversion_clear 1; constructor; auto. Qed.
   Lemma Exists_fmap (P : B → Prop) l : Exists P (f <$> l) ↔ Exists (P ∘ f) l.
-  Proof. split; induction l; inversion 1; constructor (by auto). Qed.
+  Proof. split; induction l; inversion 1; constructor; by auto. Qed.
   Lemma Forall2_fmap_l {C} (P : B → C → Prop) l1 l2 :
     Forall2 P (f <$> l1) l2 ↔ Forall2 (P ∘ f) l1 l2.
   Proof.
diff --git a/theories/mapset.v b/theories/mapset.v
index 366238c7..d7e7c445 100644
--- a/theories/mapset.v
+++ b/theories/mapset.v
@@ -5,28 +5,29 @@ elements of the unit type. Since maps enjoy extensional equality, the
 constructed finite sets do so as well. *)
 Require Export fin_map_dom.
 
-Record mapset (Mu : Type) := Mapset { mapset_car: Mu }.
+Record mapset (M : Type → Type) : Type :=
+  Mapset { mapset_car: M (unit : Type) }.
 Arguments Mapset {_} _.
 Arguments mapset_car {_} _.
 
 Section mapset.
 Context `{FinMap K M}.
 
-Instance mapset_elem_of: ElemOf K (mapset (M unit)) := λ x X,
+Instance mapset_elem_of: ElemOf K (mapset M) := λ x X,
   mapset_car X !! x = Some ().
-Instance mapset_empty: Empty (mapset (M unit)) := Mapset ∅.
-Instance mapset_singleton: Singleton K (mapset (M unit)) := λ x,
+Instance mapset_empty: Empty (mapset M) := Mapset ∅.
+Instance mapset_singleton: Singleton K (mapset M) := λ x,
   Mapset {[ (x,()) ]}.
-Instance mapset_union: Union (mapset (M unit)) := λ X1 X2,
+Instance mapset_union: Union (mapset M) := λ X1 X2,
   let (m1) := X1 in let (m2) := X2 in Mapset (m1 ∪ m2).
-Instance mapset_intersection: Intersection (mapset (M unit)) := λ X1 X2,
+Instance mapset_intersection: Intersection (mapset M) := λ X1 X2,
   let (m1) := X1 in let (m2) := X2 in Mapset (m1 ∩ m2).
-Instance mapset_difference: Difference (mapset (M unit)) := λ X1 X2,
+Instance mapset_difference: Difference (mapset M) := λ X1 X2,
   let (m1) := X1 in let (m2) := X2 in Mapset (m1 ∖ m2).
-Instance mapset_elems: Elements K (mapset (M unit)) := λ X,
+Instance mapset_elems: Elements K (mapset M) := λ X,
   let (m) := X in (map_to_list m).*1.
 
-Lemma mapset_eq (X1 X2 : mapset (M unit)) : X1 = X2 ↔ ∀ x, x ∈ X1 ↔ x ∈ X2.
+Lemma mapset_eq (X1 X2 : mapset M) : X1 = X2 ↔ ∀ x, x ∈ X1 ↔ x ∈ X2.
 Proof.
   split; [by intros ->|].
   destruct X1 as [m1], X2 as [m2]. simpl. intros E.
@@ -34,17 +35,16 @@ Proof.
 Qed.
 
 Global Instance mapset_eq_dec `{∀ m1 m2 : M unit, Decision (m1 = m2)}
-  (X1 X2 : mapset (M unit)) : Decision (X1 = X2) | 1.
+  (X1 X2 : mapset M) : Decision (X1 = X2) | 1.
 Proof.
  refine
   match X1, X2 with Mapset m1, Mapset m2 => cast_if (decide (m1 = m2)) end;
   abstract congruence.
 Defined.
-Global Instance mapset_elem_of_dec x (X : mapset (M unit)) :
-  Decision (x ∈ X) | 1.
+Global Instance mapset_elem_of_dec x (X : mapset M) : Decision (x ∈ X) | 1.
 Proof. solve_decision. Defined.
 
-Instance: Collection K (mapset (M unit)).
+Instance: Collection K (mapset M).
 Proof.
   split; [split | | ].
   * unfold empty, elem_of, mapset_empty, mapset_elem_of.
@@ -63,9 +63,9 @@ Proof.
     intros [m1] [m2] ?. simpl. rewrite lookup_difference_Some.
     destruct (m2 !! x) as [[]|]; intuition congruence.
 Qed.
-Global Instance: PartialOrder (@subseteq (mapset (M unit)) _).
+Global Instance: PartialOrder (@subseteq (mapset M) _).
 Proof. split; try apply _. intros ????. apply mapset_eq. intuition. Qed.
-Global Instance: FinCollection K (mapset (M unit)).
+Global Instance: FinCollection K (mapset M).
 Proof.
   split.
   * apply _.
@@ -78,12 +78,12 @@ Proof.
 Qed.
 
 Definition mapset_map_with {A B} (f : bool → A → option B)
-    (X : mapset (M unit)) : M A → M B :=
+    (X : mapset M) : M A → M B :=
   let (mX) := X in merge (λ x y,
     match x, y with
     | Some _, Some a => f true a | None, Some a => f false a | _, None => None
     end) mX.
-Definition mapset_dom_with {A} (f : A → bool) (m : M A) : mapset (M unit) :=
+Definition mapset_dom_with {A} (f : A → bool) (m : M A) : mapset M :=
   Mapset $ merge (λ x _,
     match x with
     | Some a => if f a then Some () else None | None => None
@@ -104,9 +104,8 @@ Proof.
   * destruct (Is_true_reflect (f a)); naive_solver.
   * naive_solver.
 Qed.
-Instance mapset_dom {A} : Dom (M A) (mapset (M unit)) :=
-  mapset_dom_with (λ _, true).
-Instance mapset_dom_spec: FinMapDom K M (mapset (M unit)).
+Instance mapset_dom {A} : Dom (M A) (mapset M) := mapset_dom_with (λ _, true).
+Instance mapset_dom_spec: FinMapDom K M (mapset M).
 Proof.
   split; try apply _. intros. unfold dom, mapset_dom, is_Some.
   rewrite elem_of_mapset_dom_with; naive_solver.
diff --git a/theories/natmap.v b/theories/natmap.v
index 4f249931..94296e39 100644
--- a/theories/natmap.v
+++ b/theories/natmap.v
@@ -255,7 +255,7 @@ Proof.
 Qed.
 
 (** Finally, we can construct sets of [nat]s satisfying extensional equality. *)
-Notation natset := (mapset (natmap unit)).
+Notation natset := (mapset natmap).
 Instance natmap_dom {A} : Dom (natmap A) natset := mapset_dom.
 Instance: FinMapDom nat natmap natset := mapset_dom_spec.
 
diff --git a/theories/nmap.v b/theories/nmap.v
index d534989e..d833c6b9 100644
--- a/theories/nmap.v
+++ b/theories/nmap.v
@@ -7,7 +7,7 @@ Require Export prelude fin_maps.
 
 Local Open Scope N_scope.
 
-Record Nmap A := NMap { Nmap_0 : option A; Nmap_pos : Pmap A }.
+Record Nmap (A : Type) : Type := NMap { Nmap_0 : option A; Nmap_pos : Pmap A }.
 Arguments Nmap_0 {_} _.
 Arguments Nmap_pos {_} _.
 Arguments NMap {_} _ _.
@@ -81,7 +81,7 @@ Qed.
 
 (** * Finite sets *)
 (** We construct sets of [N]s satisfying extensional equality. *)
-Notation Nset := (mapset (Nmap unit)).
+Notation Nset := (mapset Nmap).
 Instance Nmap_dom {A} : Dom (Nmap A) Nset := mapset_dom.
 Instance: FinMapDom N Nmap Nset := mapset_dom_spec.
 
diff --git a/theories/numbers.v b/theories/numbers.v
index d7d5ec96..886d9f76 100644
--- a/theories/numbers.v
+++ b/theories/numbers.v
@@ -28,8 +28,8 @@ 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 "`div`" := NPeano.div (at level 35) : nat_scope.
-Infix "`mod`" := NPeano.modulo (at level 35) : nat_scope.
+Infix "`div`" := Nat.div (at level 35) : nat_scope.
+Infix "`mod`" := Nat.modulo (at level 35) : nat_scope.
 
 Instance nat_eq_dec: ∀ x y : nat, Decision (x = y) := eq_nat_dec.
 Instance nat_le_dec: ∀ x y : nat, Decision (x ≤ y) := le_dec.
diff --git a/theories/optionmap.v b/theories/optionmap.v
index ff464ca0..614f96aa 100644
--- a/theories/optionmap.v
+++ b/theories/optionmap.v
@@ -80,9 +80,8 @@ Qed.
 End optionmap.
 
 (** * Finite sets *)
-Notation optionset M := (mapset (optionmap M unit)).
+Notation optionset M := (mapset (optionmap M)).
 Instance optionmap_dom {M : Type → Type} `{∀ A, Empty (M A), Merge M} {A} :
   Dom (optionmap M A) (optionset M) := mapset_dom.
 Instance optionmap_domspec `{FinMap K M} :
   FinMapDom (option K) (optionmap M) (optionset M) := mapset_dom_spec.
-
diff --git a/theories/orders.v b/theories/orders.v
index 09290008..71568318 100644
--- a/theories/orders.v
+++ b/theories/orders.v
@@ -18,7 +18,7 @@ Section orders.
   Lemma reflexive_eq `{!Reflexive R} X Y : X = Y → X ⊆ Y.
   Proof. by intros <-. Qed.
   Lemma anti_symmetric_iff `{!PartialOrder R} X Y : X = Y ↔ R X Y ∧ R Y X.
-  Proof. intuition (subst; auto). Qed.
+  Proof. split. by intros ->. by intros [??]; apply (anti_symmetric _). Qed.
   Lemma strict_spec X Y : X ⊂ Y ↔ X ⊆ Y ∧ Y ⊈ X.
   Proof. done. Qed.
   Lemma strict_include X Y : X ⊂ Y → X ⊆ Y.
diff --git a/theories/pmap.v b/theories/pmap.v
index c8c35fd6..13e3a177 100644
--- a/theories/pmap.v
+++ b/theories/pmap.v
@@ -19,7 +19,7 @@ Local Hint Extern 0 (¬@eq positive _ _) => congruence.
 not ensure canonical representations of maps. For example the empty map can
 be represented as a binary tree of an arbitrary size that contains [None] at
 all nodes. *)
-Inductive Pmap_raw A :=
+Inductive Pmap_raw (A : Type) : Type :=
   | PLeaf: Pmap_raw A
   | PNode: Pmap_raw A → option A → Pmap_raw A → Pmap_raw A.
 Arguments PLeaf {_}.
@@ -44,7 +44,7 @@ Proof.
   | PLeaf => right _
   | PNode _ (Some x) _ => left _
   | PNode l Node r => cast_if_or (go l) (go r)
-  end); clear go; abstract first [constructor (by auto)|by inversion 1].
+  end); clear go; abstract first [constructor; by auto|by inversion 1].
 Defined.
 
 (** The following predicate describes well well formed trees. A tree is well
@@ -65,12 +65,12 @@ Proof.
   | PNode l (Some x) r => cast_if_and (go l) (go r)
   | PNode l Node r =>
      cast_if_and3 (decide (Pmap_ne l ∨ Pmap_ne r)) (go l) (go r)
-  end); clear go; abstract first [constructor (by auto)|by inversion 1].
+  end); clear go; abstract first [constructor; by auto|by inversion 1].
 Defined.
 
 (** Now we restrict the data type of trees to those that are well formed and
 thereby obtain a data type that ensures canonicity. *)
-Inductive Pmap A := PMap {
+Inductive Pmap (A : Type) : Type := PMap {
   pmap_car : Pmap_raw A;
   pmap_bool_prf : bool_decide (Pmap_wf pmap_car)
 }.
@@ -387,7 +387,7 @@ Qed.
 
 (** * Finite sets *)
 (** We construct sets of [positives]s satisfying extensional equality. *)
-Notation Pset := (mapset (Pmap unit)).
+Notation Pset := (mapset Pmap).
 Instance Pmap_dom {A} : Dom (Pmap A) Pset := mapset_dom.
 Instance: FinMapDom positive Pmap Pset := mapset_dom_spec.
 
diff --git a/theories/pretty.v b/theories/pretty.v
index c5f69c04..86e4b47e 100644
--- a/theories/pretty.v
+++ b/theories/pretty.v
@@ -18,40 +18,54 @@ Definition pretty_N_char (x : N) : ascii :=
   | 0 => "0" | 1 => "1" | 2 => "2" | 3 => "3" | 4 => "4"
   | 5 => "5" | 6 => "6" | 7 => "7" | 8 => "8" | _ => "9"
   end%char%N.
-Definition pretty_N_go (x : N)
-    (go : ∀ y, (y < x)%N → string → string) (s : string) : string :=
+Fixpoint pretty_N_go_help (x : N) (acc : Acc (<)%N x) (s : string) : string :=
   match decide (0 < x)%N with
-  | left H => go (x `div` 10)%N (N.div_lt x 10 H eq_refl)
+  | left H => pretty_N_go_help (x `div` 10)%N
+     (Acc_inv acc (N.div_lt x 10 H eq_refl))
      (String (pretty_N_char (x `mod` 10)) s)
   | right _ => s
   end.
-Instance pretty_N : Pretty N := λ x,
-  Fix_F _ pretty_N_go (wf_guard 32 N.lt_wf_0 x) ""%string.
+Definition pretty_N_go (x : N) : string → string :=
+  pretty_N_go_help x (wf_guard 32 N.lt_wf_0 x).
+Lemma pretty_N_go_0 s : pretty_N_go 0 s = s.
+Proof. done. Qed.
+Lemma pretty_N_go_help_irrel x acc1 acc2 s :
+  pretty_N_go_help x acc1 s = pretty_N_go_help x acc2 s.
+Proof.
+  revert x acc1 acc2 s; fix 2; intros x [acc1] [acc2] s; simpl.
+  destruct (decide (0 < x)%N); auto.
+Qed.
+Lemma pretty_N_go_step x s :
+  (0 < x)%N → pretty_N_go x s
+  = pretty_N_go (x `div` 10) (String (pretty_N_char (x `mod` 10)) s).
+Proof.
+  unfold pretty_N_go; intros; destruct (wf_guard 32 N.lt_wf_0 x).
+  unfold pretty_N_go_help; fold pretty_N_go_help.
+  by destruct (decide (0 < x)%N); auto using pretty_N_go_help_irrel.
+Qed.
+Instance pretty_N : Pretty N := λ x, pretty_N_go x ""%string.
 Instance pretty_N_injective : Injective (@eq N) (=) pretty.
 Proof.
   assert (∀ x y, x < 10 → y < 10 →
     pretty_N_char x =  pretty_N_char y → x = y)%N.
   { compute; intros. by repeat (discriminate || case_match). }
-  set (f x (acc : Acc _ x) := Fix_F _ pretty_N_go acc).
-  cut (∀ x acc y acc' s s', length s = length s' →
-    f x acc s = f y acc' s' → x = y ∧ s = s').
+  cut (∀ x y s s', pretty_N_go x s = pretty_N_go y s' →
+    length s = length s' → x = y ∧ s = s').
   { intros help x y ?. eapply help; eauto. }
-  assert (∀ x acc s, ¬length (f x acc s) < length s) as help.
+  assert (∀ x s, ¬length (pretty_N_go x s) < length s) as help.
   { setoid_rewrite <-Nat.le_ngt.
-    fix 2; intros x [?] s; simpl. unfold pretty_N_go; fold pretty_N_go.
-    destruct (decide (0 < x))%N; [|auto].
-    etransitivity; [|eauto]. simpl; lia. }
-  fix 2; intros x [?] y [?] s s' ?; simpl.
-  unfold pretty_N_go; fold pretty_N_go; intros Hs.
-  destruct (decide (0 < x))%N, (decide (0 < y))%N;
-    try match goal with
-    | H : f ?x ?acc ?s = _ |- _ =>
-       destruct (help x acc s); rewrite H; simpl; lia
-    | H : _ = f ?x ?acc ?s |- _ =>
-       destruct (help x acc s); rewrite <-H; simpl; lia
-    end; auto with lia.
-  apply pretty_N_injective in Hs; [|by f_equal']; destruct Hs.
-  simplify_equality; split; [|done].
+    intros x; induction (N.lt_wf_0 x) as [x _ IH]; intros s.
+    assert (x = 0 ∨ 0 < x)%N as [->|?] by lia; [by rewrite pretty_N_go_0|].
+    rewrite pretty_N_go_step by done.
+    etransitivity; [|by eapply IH, N.div_lt]; simpl; lia. }
+  intros x; induction (N.lt_wf_0 x) as [x _ IH]; intros y s s'.
+  assert ((x = 0 ∨ 0 < x) ∧ (y = 0 ∨ 0 < y))%N as [[->|?] [->|?]] by lia;
+    rewrite ?pretty_N_go_0, ?pretty_N_go_step, ?(pretty_N_go_step y) by done.
+  { done. }
+  { intros -> Hlen; edestruct help; rewrite Hlen; simpl; lia. }
+  { intros <- Hlen; edestruct help; rewrite <-Hlen; simpl; lia. }
+  intros Hs Hlen; apply IH in Hs; destruct Hs;
+    simplify_equality'; split_ands'; auto using N.div_lt_upper_bound with lia.
   rewrite (N.div_mod x 10), (N.div_mod y 10) by done.
   auto using N.mod_lt with f_equal.
 Qed.
diff --git a/theories/stringmap.v b/theories/stringmap.v
index d14d6f1b..c519eff8 100644
--- a/theories/stringmap.v
+++ b/theories/stringmap.v
@@ -158,7 +158,7 @@ Qed.
 
 (** * Finite sets *)
 (** We construct sets of [strings]s satisfying extensional equality. *)
-Notation stringset := (mapset (stringmap unit)).
+Notation stringset := (mapset stringmap).
 Instance stringmap_dom {A} : Dom (stringmap A) stringset := mapset_dom.
 Instance: FinMapDom positive Pmap Pset := mapset_dom_spec.
 
diff --git a/theories/tactics.v b/theories/tactics.v
index 507e582a..73c0e9db 100644
--- a/theories/tactics.v
+++ b/theories/tactics.v
@@ -5,6 +5,19 @@ the development. *)
 Require Export Psatz.
 Require Export base.
 
+Lemma f_equal_dep {A B} (f g : ∀ x : A, B x) x : f = g → f x = g x.
+Proof. intros ->; reflexivity. Qed.
+Lemma f_equal_help {A B} (f g : A → B) x y : f = g → x = y → f x = g y.
+Proof. intros -> ->; reflexivity. Qed.
+Ltac f_equal :=
+  let rec go :=
+    match goal with
+    | _ => reflexivity
+    | _ => apply f_equal_help; [go|try reflexivity]
+    | |- ?f ?x = ?g ?x => apply (f_equal_dep f g); go
+    end in
+  try go.
+
 (** We declare hint databases [f_equal], [congruence] and [lia] and containing
 solely the tactic corresponding to its name. These hint database are useful in
 to be combined in combination with other hint database. *)
diff --git a/theories/zmap.v b/theories/zmap.v
index 42f15539..f91c7fb4 100644
--- a/theories/zmap.v
+++ b/theories/zmap.v
@@ -6,7 +6,7 @@ Require Import pmap mapset.
 Require Export prelude fin_maps.
 Local Open Scope Z_scope.
 
-Record Zmap A :=
+Record Zmap (A : Type) : Type :=
   ZMap { Zmap_0 : option A; Zmap_pos : Pmap A; Zmap_neg : Pmap A }.
 Arguments Zmap_0 {_} _.
 Arguments Zmap_pos {_} _.
@@ -92,6 +92,6 @@ Qed.
 
 (** * Finite sets *)
 (** We construct sets of [Z]s satisfying extensional equality. *)
-Notation Zset := (mapset (Zmap unit)).
+Notation Zset := (mapset Zmap).
 Instance Zmap_dom {A} : Dom (Zmap A) Zset := mapset_dom.
 Instance: FinMapDom Z Zmap Zset := mapset_dom_spec.
-- 
GitLab