From 8fd2f046234628e605473d232178d5970da9a772 Mon Sep 17 00:00:00 2001
From: Aleksandar Nanevski <aleks.nanevski@imdea.org>
Date: Tue, 10 Sep 2024 16:46:06 +0200
Subject: [PATCH 1/2] updating to coqdev

---
 core/auto.v      |  2 +-
 core/axioms.v    |  2 +-
 core/finmap.v    |  4 ++--
 core/ordtype.v   |  2 +-
 core/pred.v      |  5 ++---
 core/prelude.v   |  8 ++++----
 core/rtc.v       |  2 +-
 core/seqext.v    |  2 +-
 core/seqperm.v   |  2 +-
 core/slice.v     |  4 ++--
 core/uconsec.v   |  2 +-
 core/useqord.v   |  2 +-
 core/uslice.v    |  2 +-
 pcm/automap.v    |  2 +-
 pcm/autopcm.v    |  2 +-
 pcm/heap.v       |  2 +-
 pcm/invertible.v |  2 +-
 pcm/morphism.v   | 12 ++++++------
 pcm/mutex.v      |  4 ++--
 pcm/natmap.v     |  2 +-
 pcm/pcm.v        |  2 +-
 pcm/unionmap.v   |  2 +-
 22 files changed, 34 insertions(+), 35 deletions(-)

diff --git a/core/auto.v b/core/auto.v
index 88ebad5..cf772cf 100644
--- a/core/auto.v
+++ b/core/auto.v
@@ -11,7 +11,7 @@ See the License for the specific language governing permissions and
 limitations under the License.
 *)
 
-From Coq Require Import ssreflect ssrbool ssrfun.
+From Stdlib Require Import ssreflect ssrbool ssrfun.
 From mathcomp Require Import ssrnat seq eqtype.
 From pcm Require Import options prelude.
 
diff --git a/core/axioms.v b/core/axioms.v
index 1154652..a5ca0a6 100644
--- a/core/axioms.v
+++ b/core/axioms.v
@@ -21,7 +21,7 @@ limitations under the License.
 (* Jonh Major equality via equality cast.                                     *)
 (******************************************************************************)
 
-From Coq Require Import ssreflect ssrfun Eqdep ClassicalFacts.
+From Stdlib Require Import ssreflect ssrfun Eqdep ClassicalFacts.
 From mathcomp Require Import eqtype.
 From pcm Require Import options.
 
diff --git a/core/finmap.v b/core/finmap.v
index c54609a..d56f416 100644
--- a/core/finmap.v
+++ b/core/finmap.v
@@ -17,8 +17,8 @@ limitations under the License.
 (******************************************************************)
 
 From HB Require Import structures.
-From Coq Require Import ssreflect ssrbool ssrfun.
-From Coq Require Setoid.
+From Stdlib Require Import ssreflect ssrbool ssrfun.
+From Stdlib Require Setoid.
 From mathcomp Require Import ssrnat eqtype seq path.
 From pcm Require Export ordtype seqperm.
 From pcm Require Import options.
diff --git a/core/ordtype.v b/core/ordtype.v
index 422f73d..2b5f175 100644
--- a/core/ordtype.v
+++ b/core/ordtype.v
@@ -19,7 +19,7 @@ limitations under the License.
 (******************************************************************************)
 
 From HB Require Import structures.
-From Coq Require Import ssreflect ssrbool ssrfun.
+From Stdlib Require Import ssreflect ssrbool ssrfun.
 From mathcomp Require Import ssrnat eqtype seq path fintype.
 From pcm Require Import options seqext.
 
diff --git a/core/pred.v b/core/pred.v
index c272339..99fb54e 100644
--- a/core/pred.v
+++ b/core/pred.v
@@ -15,7 +15,7 @@ limitations under the License.
 (* This file re-implements some of ssrbool's entities in Prop universe        *)
 (******************************************************************************)
 
-From Coq Require Import ssreflect ssrbool ssrfun Setoid Basics.
+From Stdlib Require Import ssreflect ssrbool ssrfun Setoid Basics.
 From mathcomp Require Import ssrnat seq eqtype.
 From pcm Require Import options.
 
@@ -1521,7 +1521,7 @@ Definition id_rel : Rel A := fun x y => y = x.
 Lemma id_rel_refl : forall x, id_rel x x.
 Proof. by []. Qed.
 Lemma id_rel_sym : Symmetric id_rel.
-Proof. by []. Qed.
+Proof. by split. Qed.
 Lemma id_rel_trans : Transitive id_rel.
 Proof. by move=> x y z ->->. Qed.
 Lemma id_rel_func : functional id_rel.
@@ -1538,7 +1538,6 @@ Lemma pre_rel_func R P : functional R -> functional (pre_rel P R).
 Proof. by move=> funcR x y1 y2 [_ Rxy1] [_ /(funcR _ _ _ Rxy1)]. Qed.
 End PreConditionalRelation.
 
-
 (** Imposing "postcondition" on a relation *)
 Section PostConditionalRelation.
 Definition post_rel R Q := fun x y => R x y /\ Q y.
diff --git a/core/prelude.v b/core/prelude.v
index 93ace74..3b73516 100644
--- a/core/prelude.v
+++ b/core/prelude.v
@@ -17,7 +17,7 @@ limitations under the License.
 (******************************************************************************)
 
 From HB Require Import structures.
-From Coq Require Import ssreflect ssrfun Eqdep. 
+From Stdlib Require Import ssreflect ssrfun Eqdep. 
 From mathcomp Require Import ssrbool ssrnat seq eqtype choice path.
 From mathcomp Require Import fintype finset finfun tuple perm fingroup.
 From pcm Require Import options axioms.
@@ -307,8 +307,8 @@ Notation "[ \/ P1 , P2 , P3 , P4 , P5 , P6 | P7 ]" := (or7 P1 P2 P3 P4 P5 P6 P7)
 (** Add the ability to rewrite with [<->] for the custom logical connectives *)
 
 
-From Coq Require Import Classes.Morphisms Program.Basics Program.Tactics.
-From Coq Require Import Relations.
+From Stdlib Require Import Classes.Morphisms Program.Basics Program.Tactics.
+From Stdlib Require Import Relations.
 
 Local Obligation Tactic := try solve [simpl_relation | firstorder auto].
 
@@ -1274,7 +1274,7 @@ Lemma onth_tnth {n} (s : n.-tuple A) (i : 'I_n) :
 Proof.
 elim: n s i =>[|n IH] s i; first by case: i.
 case/tupleP: s=>/=x s; case: (unliftP ord0 i)=>[j|]-> /=.
-- by rewrite tnthS.
+- by rewrite tnthS add0n.
 by rewrite tnth0.
 Qed.
 
diff --git a/core/rtc.v b/core/rtc.v
index 72e7c72..ef9516e 100644
--- a/core/rtc.v
+++ b/core/rtc.v
@@ -11,7 +11,7 @@ See the License for the specific language governing permissions and
 limitations under the License.
 *)
 
-From Coq Require Import ssreflect ssrbool ssrfun.
+From Stdlib Require Import ssreflect ssrbool ssrfun.
 From mathcomp Require Import ssrnat eqtype seq choice fintype path fingraph.
 From pcm Require Import options axioms pred prelude finmap seqext.
 
diff --git a/core/seqext.v b/core/seqext.v
index 7033112..0a0096a 100644
--- a/core/seqext.v
+++ b/core/seqext.v
@@ -11,7 +11,7 @@ See the License for the specific language governing permissions and
 limitations under the License.
 *)
 
-From Coq Require Import ssreflect ssrbool ssrfun.
+From Stdlib Require Import ssreflect ssrbool ssrfun.
 From mathcomp Require Import ssrnat seq eqtype path choice fintype bigop perm.
 From pcm Require Import options prelude pred.
 
diff --git a/core/seqperm.v b/core/seqperm.v
index 962d1a7..eb61a02 100644
--- a/core/seqperm.v
+++ b/core/seqperm.v
@@ -11,7 +11,7 @@ See the License for the specific language governing permissions and
 limitations under the License.
 *)
 
-From Coq Require Import ssreflect ssrbool ssrfun.
+From Stdlib Require Import ssreflect ssrbool ssrfun.
 From mathcomp Require Import ssrnat seq path eqtype.
 From pcm Require Import options pred.
 
diff --git a/core/slice.v b/core/slice.v
index facf3f1..aa46060 100644
--- a/core/slice.v
+++ b/core/slice.v
@@ -11,7 +11,7 @@ See the License for the specific language governing permissions and
 limitations under the License.
 *)
 
-From Coq Require Import ssreflect ssrbool ssrfun.
+From Stdlib Require Import ssreflect ssrbool ssrfun.
 From mathcomp Require Import ssrnat eqtype seq path interval order.
 From mathcomp Require Import fintype finfun tuple.
 From pcm Require Import options prelude seqext.
@@ -20,7 +20,7 @@ Open Scope order_scope.
 Import Order.Theory.
 
 Section BSimp_Extension.
-Variables (disp : unit) (T : porderType disp).
+Variables (disp : Order.disp_t) (T : porderType disp).
 Implicit Types (x y : T) (b c : bool).
 
 Lemma binf_inf b c : (BInfty T b == BInfty T c) = (b == c).
diff --git a/core/uconsec.v b/core/uconsec.v
index fdfc444..d9815b1 100644
--- a/core/uconsec.v
+++ b/core/uconsec.v
@@ -11,7 +11,7 @@ See the License for the specific language governing permissions and
 limitations under the License.
 *)
 
-From Coq Require Import ssreflect ssrbool ssrfun.
+From Stdlib Require Import ssreflect ssrbool ssrfun.
 From mathcomp Require Import ssrnat eqtype seq path interval order.
 From pcm Require Import options prelude ordtype seqext slice useqord uslice.
 Local Open Scope order_scope.
diff --git a/core/useqord.v b/core/useqord.v
index d34c170..0c7c150 100644
--- a/core/useqord.v
+++ b/core/useqord.v
@@ -11,7 +11,7 @@ See the License for the specific language governing permissions and
 limitations under the License.
 *)
 
-From Coq Require Import ssreflect ssrbool ssrfun.
+From Stdlib Require Import ssreflect ssrbool ssrfun.
 From mathcomp Require Import ssrnat eqtype seq path interval order.
 From pcm Require Import options prelude ordtype seqext.
 Local Open Scope order_scope.
diff --git a/core/uslice.v b/core/uslice.v
index b17c674..ef7935c 100644
--- a/core/uslice.v
+++ b/core/uslice.v
@@ -11,7 +11,7 @@ See the License for the specific language governing permissions and
 limitations under the License.
 *)
 
-From Coq Require Import ssreflect ssrbool ssrfun.
+From Stdlib Require Import ssreflect ssrbool ssrfun.
 From mathcomp Require Import ssrnat eqtype seq path interval order.
 From pcm Require Import options prelude ordtype seqext slice useqord.
 (* We assume the sequences are unique and use the first index,  *)
diff --git a/pcm/automap.v b/pcm/automap.v
index f15f593..a3198b7 100644
--- a/pcm/automap.v
+++ b/pcm/automap.v
@@ -11,7 +11,7 @@ See the License for the specific language governing permissions and
 limitations under the License.
 *)
 
-From Coq Require Import ssreflect ssrbool ssrfun.
+From Stdlib Require Import ssreflect ssrbool ssrfun.
 From mathcomp Require Import ssrnat eqtype seq.
 From pcm Require Import options pred prelude.
 From pcm Require Export auto.
diff --git a/pcm/autopcm.v b/pcm/autopcm.v
index 8c4dea9..8448bbd 100644
--- a/pcm/autopcm.v
+++ b/pcm/autopcm.v
@@ -11,7 +11,7 @@ See the License for the specific language governing permissions and
 limitations under the License.
 *)
 
-From Coq Require Import ssreflect ssrbool ssrfun.
+From Stdlib Require Import ssreflect ssrbool ssrfun.
 From mathcomp Require Import ssrnat eqtype seq.
 From pcm Require Import options pred prelude pcm.
 From pcm Require Export auto.
diff --git a/pcm/heap.v b/pcm/heap.v
index ea4c3c1..00b7561 100644
--- a/pcm/heap.v
+++ b/pcm/heap.v
@@ -18,7 +18,7 @@ limitations under the License.
 (******************************************************************************)
 
 From HB Require Import structures.
-From Coq Require Import ssreflect ssrbool ssrfun Eqdep.
+From Stdlib Require Import ssreflect ssrbool ssrfun Eqdep.
 From mathcomp Require Import ssrnat eqtype fintype tuple finfun seq path bigop.
 From pcm Require Import options axioms prelude pred finmap.
 From pcm Require Import pcm unionmap natmap.
diff --git a/pcm/invertible.v b/pcm/invertible.v
index 89e6677..d81bdac 100644
--- a/pcm/invertible.v
+++ b/pcm/invertible.v
@@ -16,7 +16,7 @@ limitations under the License.
 (* separating relations.                                                      *)
 (******************************************************************************)
 
-From Coq Require Import ssreflect ssrbool ssrfun.
+From Stdlib Require Import ssreflect ssrbool ssrfun.
 From mathcomp Require Import eqtype.
 From pcm Require Import options axioms prelude.
 From pcm Require Import pcm morphism.
diff --git a/pcm/morphism.v b/pcm/morphism.v
index 582203b..2fa24d0 100644
--- a/pcm/morphism.v
+++ b/pcm/morphism.v
@@ -12,7 +12,7 @@ limitations under the License.
 *)
 
 From HB Require Import structures.
-From Coq Require Import ssreflect ssrbool ssrfun.
+From Stdlib Require Import ssreflect ssrbool ssrfun.
 From mathcomp Require Import ssrnat eqtype fintype finfun.
 From pcm Require Import options pred axioms prelude.
 From pcm Require Import pcm.
@@ -1584,8 +1584,8 @@ HB.instance Definition _ (f : full_binorm_pcm_morph U V)
                          (g : full_binorm_pcm_morph V W) :=
   Full_Binorm_PCM_morphism.copy (g \o f) 
     (Full_Binorm_PCM_morphism.pack_ 
-       (Binorm_PCM_morphism.class (g \o f))
        (Norm_PCM_morphism.class (g \o f))
+       (Binorm_PCM_morphism.class (g \o f))
        (Full_PCM_morphism.class (g \o f))).
 
 End CompMorphism.
@@ -1822,8 +1822,8 @@ HB.instance Definition _
   Binorm_TPCM_morphism.copy (g \o f) 
     (Binorm_TPCM_morphism.pack_ 
        (TPCM_morphism.class (g \o f))
-       (Binorm_PCM_morphism.class (g \o f))
-       (Norm_PCM_morphism.class (g \o f))).
+       (Norm_PCM_morphism.class (g \o f))
+       (Binorm_PCM_morphism.class (g \o f))).
 
 HB.instance Definition _ 
   (f : full_tpcm_morph U V) (g : full_tpcm_morph V W) :=
@@ -1846,8 +1846,8 @@ HB.instance Definition _
     (Full_Binorm_TPCM_morphism.pack_ 
        (TPCM_morphism.class (g \o f))
        (Full_PCM_morphism.class (g \o f))
-       (Binorm_PCM_morphism.class (g \o f))
-       (Norm_PCM_morphism.class (g \o f))).
+       (Norm_PCM_morphism.class (g \o f))
+       (Binorm_PCM_morphism.class (g \o f))).
 
 End Comp. 
 
diff --git a/pcm/mutex.v b/pcm/mutex.v
index ef6c6c2..3aad0b8 100644
--- a/pcm/mutex.v
+++ b/pcm/mutex.v
@@ -20,8 +20,8 @@ limitations under the License.
 (******************************************************************************)
 
 From HB Require Import structures.
-From Coq Require Import ssreflect ssrbool ssrfun.
-From Coq Require Setoid.
+From Stdlib Require Import ssreflect ssrbool ssrfun.
+From Stdlib Require Setoid.
 From mathcomp Require Import ssrnat eqtype seq.
 From pcm Require Import options prelude pred.
 From pcm Require Import pcm morphism natmap.
diff --git a/pcm/natmap.v b/pcm/natmap.v
index e12b8ad..68aa27d 100644
--- a/pcm/natmap.v
+++ b/pcm/natmap.v
@@ -19,7 +19,7 @@ limitations under the License.
 (******************************************************************************)
 
 From HB Require Import structures.
-From Coq Require Import ssreflect ssrbool ssrfun.
+From Stdlib Require Import ssreflect ssrbool ssrfun.
 From mathcomp Require Import ssrnat eqtype seq path interval.
 From pcm Require Import axioms options prelude pred finmap rtc seqext.
 From pcm Require Export useqord uslice uconsec pcm morphism unionmap.
diff --git a/pcm/pcm.v b/pcm/pcm.v
index b0817d5..0e35d35 100644
--- a/pcm/pcm.v
+++ b/pcm/pcm.v
@@ -18,7 +18,7 @@ limitations under the License.
 (******************************************************************************)
 
 From HB Require Import structures.
-From Coq Require Import ssreflect ssrbool ssrfun Setoid.
+From Stdlib Require Import ssreflect ssrbool ssrfun Setoid.
 From mathcomp Require Import ssrnat eqtype seq bigop fintype finset finfun.
 From pcm Require Import options axioms prelude seqperm pred seqext.
 
diff --git a/pcm/unionmap.v b/pcm/unionmap.v
index 0e92741..5c1dd49 100644
--- a/pcm/unionmap.v
+++ b/pcm/unionmap.v
@@ -91,7 +91,7 @@ limitations under the License.
 (******************************************************************************)
 
 From HB Require Import structures.
-From Coq Require Import ssreflect ssrbool ssrfun.
+From Stdlib Require Import ssreflect ssrbool ssrfun.
 From mathcomp Require Import ssrnat eqtype seq path bigop.
 From pcm Require Import options axioms prelude finmap seqperm pred seqext.
 From pcm Require Export ordtype.

From 8c51edd25e5695137df4154d5c0fc09eccfe69b5 Mon Sep 17 00:00:00 2001
From: Aleksandar Nanevski <aleks.nanevski@imdea.org>
Date: Tue, 17 Sep 2024 13:33:10 +0200
Subject: [PATCH 2/2] preparing v2.0 for release

---
 _CoqProject      |   4 ++
 core/auto.v      |   2 +-
 core/axioms.v    |   2 +-
 core/finmap.v    |   4 +-
 core/ordtype.v   |   2 +-
 core/pred.v      |   3 +-
 core/prelude.v   |   8 ++--
 core/rtc.v       |   2 +-
 core/seqext.v    |   2 +-
 core/seqperm.v   |   2 +-
 core/slice.v     |   4 +-
 core/uconsec.v   |   2 +-
 core/useqord.v   |   2 +-
 core/uslice.v    |   2 +-
 pcm/automap.v    |   2 +-
 pcm/autopcm.v    |   2 +-
 pcm/heap.v       |   2 +-
 pcm/invertible.v |   2 +-
 pcm/morphism.v   | 100 ++++++++++++++++++++++++++---------------------
 pcm/mutex.v      |   4 +-
 pcm/natmap.v     |   2 +-
 pcm/pcm.v        |   2 +-
 pcm/unionmap.v   |   2 +-
 23 files changed, 87 insertions(+), 72 deletions(-)

diff --git a/_CoqProject b/_CoqProject
index e337ff1..f796504 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -1,6 +1,10 @@
 -Q . pcm
 -arg -w -arg -notation-overridden
 -arg -w -arg -redundant-canonical-projection
+# release-specific args
+-arg -w -arg -notation-incompatible-prefix # specific to coq8.20.0 
+-arg -w -arg -deprecated-from-Coq # specific to coq8.21 
+-arg -w -arg -deprecated-dirpath-Coq # specific to coq8.21 
 
 core/options.v
 core/axioms.v
diff --git a/core/auto.v b/core/auto.v
index cf772cf..88ebad5 100644
--- a/core/auto.v
+++ b/core/auto.v
@@ -11,7 +11,7 @@ See the License for the specific language governing permissions and
 limitations under the License.
 *)
 
-From Stdlib Require Import ssreflect ssrbool ssrfun.
+From Coq Require Import ssreflect ssrbool ssrfun.
 From mathcomp Require Import ssrnat seq eqtype.
 From pcm Require Import options prelude.
 
diff --git a/core/axioms.v b/core/axioms.v
index a5ca0a6..1154652 100644
--- a/core/axioms.v
+++ b/core/axioms.v
@@ -21,7 +21,7 @@ limitations under the License.
 (* Jonh Major equality via equality cast.                                     *)
 (******************************************************************************)
 
-From Stdlib Require Import ssreflect ssrfun Eqdep ClassicalFacts.
+From Coq Require Import ssreflect ssrfun Eqdep ClassicalFacts.
 From mathcomp Require Import eqtype.
 From pcm Require Import options.
 
diff --git a/core/finmap.v b/core/finmap.v
index d56f416..c54609a 100644
--- a/core/finmap.v
+++ b/core/finmap.v
@@ -17,8 +17,8 @@ limitations under the License.
 (******************************************************************)
 
 From HB Require Import structures.
-From Stdlib Require Import ssreflect ssrbool ssrfun.
-From Stdlib Require Setoid.
+From Coq Require Import ssreflect ssrbool ssrfun.
+From Coq Require Setoid.
 From mathcomp Require Import ssrnat eqtype seq path.
 From pcm Require Export ordtype seqperm.
 From pcm Require Import options.
diff --git a/core/ordtype.v b/core/ordtype.v
index 2b5f175..422f73d 100644
--- a/core/ordtype.v
+++ b/core/ordtype.v
@@ -19,7 +19,7 @@ limitations under the License.
 (******************************************************************************)
 
 From HB Require Import structures.
-From Stdlib Require Import ssreflect ssrbool ssrfun.
+From Coq Require Import ssreflect ssrbool ssrfun.
 From mathcomp Require Import ssrnat eqtype seq path fintype.
 From pcm Require Import options seqext.
 
diff --git a/core/pred.v b/core/pred.v
index 99fb54e..b98befc 100644
--- a/core/pred.v
+++ b/core/pred.v
@@ -15,7 +15,7 @@ limitations under the License.
 (* This file re-implements some of ssrbool's entities in Prop universe        *)
 (******************************************************************************)
 
-From Stdlib Require Import ssreflect ssrbool ssrfun Setoid Basics.
+From Coq Require Import ssreflect ssrbool ssrfun Setoid Basics.
 From mathcomp Require Import ssrnat seq eqtype.
 From pcm Require Import options.
 
@@ -1538,6 +1538,7 @@ Lemma pre_rel_func R P : functional R -> functional (pre_rel P R).
 Proof. by move=> funcR x y1 y2 [_ Rxy1] [_ /(funcR _ _ _ Rxy1)]. Qed.
 End PreConditionalRelation.
 
+
 (** Imposing "postcondition" on a relation *)
 Section PostConditionalRelation.
 Definition post_rel R Q := fun x y => R x y /\ Q y.
diff --git a/core/prelude.v b/core/prelude.v
index 3b73516..16ba856 100644
--- a/core/prelude.v
+++ b/core/prelude.v
@@ -17,7 +17,7 @@ limitations under the License.
 (******************************************************************************)
 
 From HB Require Import structures.
-From Stdlib Require Import ssreflect ssrfun Eqdep. 
+From Coq Require Import ssreflect ssrfun Eqdep. 
 From mathcomp Require Import ssrbool ssrnat seq eqtype choice path.
 From mathcomp Require Import fintype finset finfun tuple perm fingroup.
 From pcm Require Import options axioms.
@@ -307,8 +307,8 @@ Notation "[ \/ P1 , P2 , P3 , P4 , P5 , P6 | P7 ]" := (or7 P1 P2 P3 P4 P5 P6 P7)
 (** Add the ability to rewrite with [<->] for the custom logical connectives *)
 
 
-From Stdlib Require Import Classes.Morphisms Program.Basics Program.Tactics.
-From Stdlib Require Import Relations.
+From Coq Require Import Classes.Morphisms Program.Basics Program.Tactics.
+From Coq Require Import Relations.
 
 Local Obligation Tactic := try solve [simpl_relation | firstorder auto].
 
@@ -1274,7 +1274,7 @@ Lemma onth_tnth {n} (s : n.-tuple A) (i : 'I_n) :
 Proof.
 elim: n s i =>[|n IH] s i; first by case: i.
 case/tupleP: s=>/=x s; case: (unliftP ord0 i)=>[j|]-> /=.
-- by rewrite tnthS add0n.
+- by rewrite tnthS ?add0n.
 by rewrite tnth0.
 Qed.
 
diff --git a/core/rtc.v b/core/rtc.v
index ef9516e..72e7c72 100644
--- a/core/rtc.v
+++ b/core/rtc.v
@@ -11,7 +11,7 @@ See the License for the specific language governing permissions and
 limitations under the License.
 *)
 
-From Stdlib Require Import ssreflect ssrbool ssrfun.
+From Coq Require Import ssreflect ssrbool ssrfun.
 From mathcomp Require Import ssrnat eqtype seq choice fintype path fingraph.
 From pcm Require Import options axioms pred prelude finmap seqext.
 
diff --git a/core/seqext.v b/core/seqext.v
index 0a0096a..7033112 100644
--- a/core/seqext.v
+++ b/core/seqext.v
@@ -11,7 +11,7 @@ See the License for the specific language governing permissions and
 limitations under the License.
 *)
 
-From Stdlib Require Import ssreflect ssrbool ssrfun.
+From Coq Require Import ssreflect ssrbool ssrfun.
 From mathcomp Require Import ssrnat seq eqtype path choice fintype bigop perm.
 From pcm Require Import options prelude pred.
 
diff --git a/core/seqperm.v b/core/seqperm.v
index eb61a02..962d1a7 100644
--- a/core/seqperm.v
+++ b/core/seqperm.v
@@ -11,7 +11,7 @@ See the License for the specific language governing permissions and
 limitations under the License.
 *)
 
-From Stdlib Require Import ssreflect ssrbool ssrfun.
+From Coq Require Import ssreflect ssrbool ssrfun.
 From mathcomp Require Import ssrnat seq path eqtype.
 From pcm Require Import options pred.
 
diff --git a/core/slice.v b/core/slice.v
index aa46060..f73a15e 100644
--- a/core/slice.v
+++ b/core/slice.v
@@ -11,7 +11,7 @@ See the License for the specific language governing permissions and
 limitations under the License.
 *)
 
-From Stdlib Require Import ssreflect ssrbool ssrfun.
+From Coq Require Import ssreflect ssrbool ssrfun.
 From mathcomp Require Import ssrnat eqtype seq path interval order.
 From mathcomp Require Import fintype finfun tuple.
 From pcm Require Import options prelude seqext.
@@ -20,7 +20,7 @@ Open Scope order_scope.
 Import Order.Theory.
 
 Section BSimp_Extension.
-Variables (disp : Order.disp_t) (T : porderType disp).
+Context disp (T : porderType disp).
 Implicit Types (x y : T) (b c : bool).
 
 Lemma binf_inf b c : (BInfty T b == BInfty T c) = (b == c).
diff --git a/core/uconsec.v b/core/uconsec.v
index d9815b1..fdfc444 100644
--- a/core/uconsec.v
+++ b/core/uconsec.v
@@ -11,7 +11,7 @@ See the License for the specific language governing permissions and
 limitations under the License.
 *)
 
-From Stdlib Require Import ssreflect ssrbool ssrfun.
+From Coq Require Import ssreflect ssrbool ssrfun.
 From mathcomp Require Import ssrnat eqtype seq path interval order.
 From pcm Require Import options prelude ordtype seqext slice useqord uslice.
 Local Open Scope order_scope.
diff --git a/core/useqord.v b/core/useqord.v
index 0c7c150..d34c170 100644
--- a/core/useqord.v
+++ b/core/useqord.v
@@ -11,7 +11,7 @@ See the License for the specific language governing permissions and
 limitations under the License.
 *)
 
-From Stdlib Require Import ssreflect ssrbool ssrfun.
+From Coq Require Import ssreflect ssrbool ssrfun.
 From mathcomp Require Import ssrnat eqtype seq path interval order.
 From pcm Require Import options prelude ordtype seqext.
 Local Open Scope order_scope.
diff --git a/core/uslice.v b/core/uslice.v
index ef7935c..b17c674 100644
--- a/core/uslice.v
+++ b/core/uslice.v
@@ -11,7 +11,7 @@ See the License for the specific language governing permissions and
 limitations under the License.
 *)
 
-From Stdlib Require Import ssreflect ssrbool ssrfun.
+From Coq Require Import ssreflect ssrbool ssrfun.
 From mathcomp Require Import ssrnat eqtype seq path interval order.
 From pcm Require Import options prelude ordtype seqext slice useqord.
 (* We assume the sequences are unique and use the first index,  *)
diff --git a/pcm/automap.v b/pcm/automap.v
index a3198b7..f15f593 100644
--- a/pcm/automap.v
+++ b/pcm/automap.v
@@ -11,7 +11,7 @@ See the License for the specific language governing permissions and
 limitations under the License.
 *)
 
-From Stdlib Require Import ssreflect ssrbool ssrfun.
+From Coq Require Import ssreflect ssrbool ssrfun.
 From mathcomp Require Import ssrnat eqtype seq.
 From pcm Require Import options pred prelude.
 From pcm Require Export auto.
diff --git a/pcm/autopcm.v b/pcm/autopcm.v
index 8448bbd..8c4dea9 100644
--- a/pcm/autopcm.v
+++ b/pcm/autopcm.v
@@ -11,7 +11,7 @@ See the License for the specific language governing permissions and
 limitations under the License.
 *)
 
-From Stdlib Require Import ssreflect ssrbool ssrfun.
+From Coq Require Import ssreflect ssrbool ssrfun.
 From mathcomp Require Import ssrnat eqtype seq.
 From pcm Require Import options pred prelude pcm.
 From pcm Require Export auto.
diff --git a/pcm/heap.v b/pcm/heap.v
index 00b7561..ea4c3c1 100644
--- a/pcm/heap.v
+++ b/pcm/heap.v
@@ -18,7 +18,7 @@ limitations under the License.
 (******************************************************************************)
 
 From HB Require Import structures.
-From Stdlib Require Import ssreflect ssrbool ssrfun Eqdep.
+From Coq Require Import ssreflect ssrbool ssrfun Eqdep.
 From mathcomp Require Import ssrnat eqtype fintype tuple finfun seq path bigop.
 From pcm Require Import options axioms prelude pred finmap.
 From pcm Require Import pcm unionmap natmap.
diff --git a/pcm/invertible.v b/pcm/invertible.v
index d81bdac..89e6677 100644
--- a/pcm/invertible.v
+++ b/pcm/invertible.v
@@ -16,7 +16,7 @@ limitations under the License.
 (* separating relations.                                                      *)
 (******************************************************************************)
 
-From Stdlib Require Import ssreflect ssrbool ssrfun.
+From Coq Require Import ssreflect ssrbool ssrfun.
 From mathcomp Require Import eqtype.
 From pcm Require Import options axioms prelude.
 From pcm Require Import pcm morphism.
diff --git a/pcm/morphism.v b/pcm/morphism.v
index 2fa24d0..4b31df6 100644
--- a/pcm/morphism.v
+++ b/pcm/morphism.v
@@ -12,7 +12,7 @@ limitations under the License.
 *)
 
 From HB Require Import structures.
-From Stdlib Require Import ssreflect ssrbool ssrfun.
+From Coq Require Import ssreflect ssrbool ssrfun.
 From mathcomp Require Import ssrnat eqtype fintype finfun.
 From pcm Require Import options pred axioms prelude.
 From pcm Require Import pcm.
@@ -1571,22 +1571,26 @@ HB.instance Definition _ :=
   isFull_PCM_morphism.Build U W (g \o f) comp_is_full_morphism.
 End FullCompIsFull.
 
-(* instances for combinations must be declared explicitly *)
+(* instances for combinations must declare PCM_morphism.on *)
+(* before declaring fullness structure. *)
 
-HB.instance Definition _ (f : full_norm_pcm_morph U V) 
-                         (g : full_norm_pcm_morph V W) :=
-  Full_Norm_PCM_morphism.copy (g \o f) 
-    (Full_Norm_PCM_morphism.pack_ 
-       (Norm_PCM_morphism.class (g \o f))
-       (Full_PCM_morphism.class (g \o f))).
+HB.instance Definition _  
+    (f : full_norm_pcm_morph U V) 
+    (g : full_norm_pcm_morph V W) := 
+  PCM_morphism.on (g \o f).
+HB.instance Definition _ 
+    (f : full_norm_pcm_morph U V) 
+    (g : full_norm_pcm_morph V W) := 
+  Full_Norm_PCM_morphism.on (g \o f).
 
-HB.instance Definition _ (f : full_binorm_pcm_morph U V) 
-                         (g : full_binorm_pcm_morph V W) :=
-  Full_Binorm_PCM_morphism.copy (g \o f) 
-    (Full_Binorm_PCM_morphism.pack_ 
-       (Norm_PCM_morphism.class (g \o f))
-       (Binorm_PCM_morphism.class (g \o f))
-       (Full_PCM_morphism.class (g \o f))).
+HB.instance Definition _ 
+    (f : full_binorm_pcm_morph U V) 
+    (g : full_binorm_pcm_morph V W) :=
+  PCM_morphism.on (g \o f).
+HB.instance Definition _ 
+    (f : full_binorm_pcm_morph U V) 
+    (g : full_binorm_pcm_morph V W) :=
+  Full_Binorm_PCM_morphism.on (g \o f).
 
 End CompMorphism.
 
@@ -1811,43 +1815,49 @@ End CompTPCM.
 (* combinations declared explicitly *)
 
 HB.instance Definition _ 
-  (f : norm_tpcm_morph U V) (g : norm_tpcm_morph V W) :=
-  Norm_TPCM_morphism.copy (g \o f) 
-    (Norm_TPCM_morphism.pack_ 
-       (TPCM_morphism.class (g \o f))
-       (Norm_PCM_morphism.class (g \o f))).
-
+    (f : norm_tpcm_morph U V) 
+    (g : norm_tpcm_morph V W) :=
+  PCM_morphism.on (g \o f).
 HB.instance Definition _ 
-  (f : binorm_tpcm_morph U V) (g : binorm_tpcm_morph V W) :=
-  Binorm_TPCM_morphism.copy (g \o f) 
-    (Binorm_TPCM_morphism.pack_ 
-       (TPCM_morphism.class (g \o f))
-       (Norm_PCM_morphism.class (g \o f))
-       (Binorm_PCM_morphism.class (g \o f))).
+    (f : norm_tpcm_morph U V) 
+    (g : norm_tpcm_morph V W) :=
+  Norm_TPCM_morphism.on (g \o f).
 
 HB.instance Definition _ 
-  (f : full_tpcm_morph U V) (g : full_tpcm_morph V W) :=
-  Full_TPCM_morphism.copy (g \o f) 
-    (Full_TPCM_morphism.pack_ 
-       (TPCM_morphism.class (g \o f))
-       (Full_PCM_morphism.class (g \o f))).
+    (f : binorm_tpcm_morph U V) 
+    (g : binorm_tpcm_morph V W) :=
+  PCM_morphism.on (g \o f).
+HB.instance Definition _ 
+    (f : binorm_tpcm_morph U V) 
+    (g : binorm_tpcm_morph V W) :=
+  Binorm_TPCM_morphism.on (g \o f).
 
 HB.instance Definition _ 
-  (f : full_norm_tpcm_morph U V) (g : full_norm_tpcm_morph V W) :=
-  Full_Norm_TPCM_morphism.copy (g \o f) 
-    (Full_Norm_TPCM_morphism.pack_ 
-       (TPCM_morphism.class (g \o f))
-       (Full_PCM_morphism.class (g \o f))
-       (Norm_PCM_morphism.class (g \o f))).
+    (f : full_tpcm_morph U V) 
+    (g : full_tpcm_morph V W) :=
+  PCM_morphism.on (g \o f).
+HB.instance Definition _ 
+    (f : full_tpcm_morph U V) 
+    (g : full_tpcm_morph V W) :=
+  Full_TPCM_morphism.on (g \o f).
 
 HB.instance Definition _ 
-  (f : full_binorm_tpcm_morph U V) (g : full_binorm_tpcm_morph V W) :=
-  Full_Binorm_TPCM_morphism.copy (g \o f) 
-    (Full_Binorm_TPCM_morphism.pack_ 
-       (TPCM_morphism.class (g \o f))
-       (Full_PCM_morphism.class (g \o f))
-       (Norm_PCM_morphism.class (g \o f))
-       (Binorm_PCM_morphism.class (g \o f))).
+    (f : full_norm_tpcm_morph U V) 
+    (g : full_norm_tpcm_morph V W) :=
+  PCM_morphism.on (g \o f).
+HB.instance Definition _ 
+    (f : full_norm_tpcm_morph U V) 
+    (g : full_norm_tpcm_morph V W) :=
+  Full_Norm_TPCM_morphism.on (g \o f).
+
+HB.instance Definition _  
+    (f : full_binorm_tpcm_morph U V) 
+    (g : full_binorm_tpcm_morph V W) :=
+  PCM_morphism.on (g \o f).
+HB.instance Definition _ 
+    (f : full_binorm_tpcm_morph U V) 
+    (g : full_binorm_tpcm_morph V W) :=
+  Full_Binorm_TPCM_morphism.on (g \o f).
 
 End Comp. 
 
diff --git a/pcm/mutex.v b/pcm/mutex.v
index 3aad0b8..ef6c6c2 100644
--- a/pcm/mutex.v
+++ b/pcm/mutex.v
@@ -20,8 +20,8 @@ limitations under the License.
 (******************************************************************************)
 
 From HB Require Import structures.
-From Stdlib Require Import ssreflect ssrbool ssrfun.
-From Stdlib Require Setoid.
+From Coq Require Import ssreflect ssrbool ssrfun.
+From Coq Require Setoid.
 From mathcomp Require Import ssrnat eqtype seq.
 From pcm Require Import options prelude pred.
 From pcm Require Import pcm morphism natmap.
diff --git a/pcm/natmap.v b/pcm/natmap.v
index 68aa27d..e12b8ad 100644
--- a/pcm/natmap.v
+++ b/pcm/natmap.v
@@ -19,7 +19,7 @@ limitations under the License.
 (******************************************************************************)
 
 From HB Require Import structures.
-From Stdlib Require Import ssreflect ssrbool ssrfun.
+From Coq Require Import ssreflect ssrbool ssrfun.
 From mathcomp Require Import ssrnat eqtype seq path interval.
 From pcm Require Import axioms options prelude pred finmap rtc seqext.
 From pcm Require Export useqord uslice uconsec pcm morphism unionmap.
diff --git a/pcm/pcm.v b/pcm/pcm.v
index 0e35d35..b0817d5 100644
--- a/pcm/pcm.v
+++ b/pcm/pcm.v
@@ -18,7 +18,7 @@ limitations under the License.
 (******************************************************************************)
 
 From HB Require Import structures.
-From Stdlib Require Import ssreflect ssrbool ssrfun Setoid.
+From Coq Require Import ssreflect ssrbool ssrfun Setoid.
 From mathcomp Require Import ssrnat eqtype seq bigop fintype finset finfun.
 From pcm Require Import options axioms prelude seqperm pred seqext.
 
diff --git a/pcm/unionmap.v b/pcm/unionmap.v
index 5c1dd49..0e92741 100644
--- a/pcm/unionmap.v
+++ b/pcm/unionmap.v
@@ -91,7 +91,7 @@ limitations under the License.
 (******************************************************************************)
 
 From HB Require Import structures.
-From Stdlib Require Import ssreflect ssrbool ssrfun.
+From Coq Require Import ssreflect ssrbool ssrfun.
 From mathcomp Require Import ssrnat eqtype seq path bigop.
 From pcm Require Import options axioms prelude finmap seqperm pred seqext.
 From pcm Require Export ordtype.