diff --git a/Makefile b/Makefile
index cfe38b1..75ae33b 100644
--- a/Makefile
+++ b/Makefile
@@ -7,7 +7,7 @@
 ##         #     GNU Lesser General Public License Version 2.1          ##
 ##         #     (see LICENSE file for the text of the license)         ##
 ##########################################################################
-## GNUMakefile for Coq 8.19.2
+## GNUMakefile for Coq 8.20.0
 
 # For debugging purposes (must stay here, don't move below)
 INITIAL_VARS := $(.VARIABLES)
@@ -278,7 +278,7 @@ COQDOCLIBS?=$(COQLIBS_NOML)
 # The version of Coq being run and the version of coq_makefile that
 # generated this makefile
 COQ_VERSION:=$(shell $(COQC) --print-version | cut -d " " -f 1)
-COQMAKEFILE_VERSION:=8.19.2
+COQMAKEFILE_VERSION:=8.20.0
 
 # COQ_SRC_SUBDIRS is for user-overriding, usually to add
 # `user-contrib/Foo` to the includes, we keep COQCORE_SRC_SUBDIRS for
@@ -309,7 +309,7 @@ endif
 
 ifneq (,$(PROFILING))
   PROFILE_ARG=-profile $<.prof.json
-  PROFILE_ZIP=gzip $<.prof.json
+  PROFILE_ZIP=gzip -f $<.prof.json
 else
   PROFILE_ARG=
   PROFILE_ZIP=true
@@ -503,37 +503,6 @@ bytefiles: $(CMOFILES) $(CMAFILES)
 optfiles: $(if $(DO_NATDYNLINK),$(CMXSFILES))
 .PHONY: optfiles
 
-# FIXME, see Ralf's bugreport
-# quick is deprecated, now renamed vio
-vio: $(VOFILES:.vo=.vio)
-.PHONY: vio
-quick: vio
-	$(warning "'make quick' is deprecated, use 'make vio' or consider using 'vos' files")
-.PHONY: quick
-
-vio2vo:
-	$(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) \
-		-schedule-vio2vo $(J) $(VOFILES:%.vo=%.vio)
-.PHONY: vio2vo
-
-# quick2vo is undocumented
-quick2vo:
-	$(HIDE)make -j $(J) vio
-	$(HIDE)VIOFILES=$$(for vofile in $(VOFILES); do \
-	  viofile="$$(echo "$$vofile" | sed "s/\.vo$$/.vio/")"; \
-	  if [ "$$vofile" -ot "$$viofile" -o ! -e "$$vofile" ]; then printf "$$viofile "; fi; \
-	done); \
-	echo "VIO2VO: $$VIOFILES"; \
-	if [ -n "$$VIOFILES" ]; then \
-	  $(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) -schedule-vio2vo $(J) $$VIOFILES; \
-	fi
-.PHONY: quick2vo
-
-checkproofs:
-	$(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) \
-		-schedule-vio-checking $(J) $(VOFILES:%.vo=%.vio)
-.PHONY: checkproofs
-
 vos: $(VOFILES:%.vo=%.vos)
 .PHONY: vos
 
@@ -711,9 +680,10 @@ clean::
 	$(HIDE)rm -f $(NATIVEFILES)
 	$(HIDE)find . -name .coq-native -type d -empty -delete
 	$(HIDE)rm -f $(VOFILES)
-	$(HIDE)rm -f $(VOFILES:.vo=.vio)
 	$(HIDE)rm -f $(VOFILES:.vo=.vos)
 	$(HIDE)rm -f $(VOFILES:.vo=.vok)
+	$(HIDE)rm -f $(VOFILES:.vo=.v.prof.json)
+	$(HIDE)rm -f $(VOFILES:.vo=.v.prof.json.gz)
 	$(HIDE)rm -f $(BEAUTYFILES) $(VFILES:=.old)
 	$(HIDE)rm -f all.ps all-gal.ps all.pdf all-gal.pdf all.glob all-mli.tex
 	$(HIDE)rm -f $(VFILES:.v=.glob)
@@ -846,10 +816,6 @@ endif
 
 $(foreach vfile,$(VFILES:.v=),$(eval $(call globvorule,$(vfile))))
 
-$(VFILES:.v=.vio): %.vio: %.v
-	$(SHOW)COQC -vio $<
-	$(HIDE)$(TIMER) $(COQC) -vio $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $<
-
 $(VFILES:.v=.vos): %.vos: %.v
 	$(SHOW)COQC -vos $<
 	$(HIDE)$(TIMER) $(COQC) -vos $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $<
diff --git a/_CoqProject b/_CoqProject
index 870b910..9124b21 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -4,6 +4,7 @@
 -arg -w -arg -redundant-canonical-projection
 -arg -w -arg -deprecated-since-8.19
 -arg -w -arg -projection-no-head-constant
+-arg -w -arg -notation-incompatible-prefix
 theories/fps/directed.v
 theories/fps/invlim.v
 theories/fps/dirlim.v
diff --git a/theories/fps/directed.v b/theories/fps/directed.v
index a4cb1f8..5a6377c 100644
--- a/theories/fps/directed.v
+++ b/theories/fps/directed.v
@@ -39,7 +39,7 @@ Definition directed (T : Type) (R : T -> T -> bool) :=
   forall x y : T, { z | R x z & R y z }.
 
 (** TODO : I'm not using anti-symmetry, i.e.: directed sets can be preorders *)
-HB.mixin Record Directed (d : unit) T of Order.POrder d T := {
+HB.mixin Record Directed d T of Order.POrder d T := {
   directedP : directed (T := T) <=%O
 }.
 #[short(type="dirType")]
diff --git a/theories/fps/dirlim.v b/theories/fps/dirlim.v
index 1a31be7..ea2d26b 100644
--- a/theories/fps/dirlim.v
+++ b/theories/fps/dirlim.v
@@ -41,9 +41,8 @@ Unset Printing Implicit Defensive.
 
 #[key="dlT"]
 HB.factory Record isDirLim_classical
-    (disp : unit) (I : dirType disp)
-    (Obj : I -> Type)
-    (bonding : forall i j, i <= j -> Obj i -> Obj j)
+    disp (I : dirType disp)
+    (Obj : I -> Type) (bonding : forall i j, i <= j -> Obj i -> Obj j)
     (Sys : is_dirsys bonding)
   dlT of Choice dlT := {
     dirlim_inj i : Obj i -> dlT;
@@ -57,9 +56,8 @@ HB.factory Record isDirLim_classical
         ind =1 dirlim_ind T f Hcone
   }.
 HB.builders Context
-    (disp : unit) (I : dirType disp)
-    (Obj : I -> Type)
-    (bonding : forall i j, i <= j -> Obj i -> Obj j)
+    disp (I : dirType disp)
+    (Obj : I -> Type) (bonding : forall i j, i <= j -> Obj i -> Obj j)
     (Sys : is_dirsys bonding)
   dlT of isDirLim_classical disp I Obj bonding Sys dlT.
 
@@ -118,7 +116,7 @@ HB.end.
 
 Section DirSysCongr.
 
-Variables (disp : unit) (I : dirType disp).
+Variables (disp : _) (I : dirType disp).
 Variable Obj : I -> Type.
 Variable bonding : forall i j, i <= j -> Obj i -> Obj j.
 Variable Sys : is_dirsys bonding.
@@ -181,13 +179,13 @@ Open Scope ring_scope.
 
 
 HB.factory Record DirLim_isUnitRingDirLim
-    (disp : unit) (I : dirType disp)
+    disp (I : dirType disp)
     (Obj : I -> unitRingType)
     (bonding : forall i j, i <= j -> {rmorphism Obj i -> Obj j})
     (Sys : is_dirsys bonding)
   dlT of DirLim _ Sys dlT := {}.
 HB.builders Context
-    (disp : unit) (I : dirType disp)
+    disp (I : dirType disp)
     (Obj : I -> unitRingType)
     (bonding : forall i j, i <= j -> {rmorphism Obj i -> Obj j})
     (Sys : is_dirsys bonding)
@@ -221,13 +219,13 @@ HB.end.
 
 
 HB.factory Record DirLim_isComUnitRingDirLim
-    (disp : unit) (I : dirType disp)
+    disp (I : dirType disp)
     (Obj : I -> comUnitRingType)
     (bonding : forall i j, i <= j -> {rmorphism Obj i -> Obj j})
     (Sys : is_dirsys bonding)
   dlT of DirLim _ Sys dlT := {}.
 HB.builders Context
-    (disp : unit) (I : dirType disp)
+    disp (I : dirType disp)
     (Obj : I -> comUnitRingType)
     (bonding : forall i j, i <= j -> {rmorphism Obj i -> Obj j})
     (Sys : is_dirsys bonding)
@@ -240,13 +238,13 @@ HB.end.
 
 
 HB.factory Record DirLim_isIDomainDirLim
-    (disp : unit) (I : dirType disp)
+    disp (I : dirType disp)
     (Obj : I -> idomainType)
     (bonding : forall i j, i <= j -> {rmorphism Obj i -> Obj j})
     (Sys : is_dirsys bonding)
   dlT of DirLim _ Sys dlT := {}.
 HB.builders Context
-    (disp : unit) (I : dirType disp)
+    disp (I : dirType disp)
     (Obj : I -> idomainType)
     (bonding : forall i j, i <= j -> {rmorphism Obj i -> Obj j})
     (Sys : is_dirsys bonding)
@@ -263,13 +261,13 @@ HB.end.
 
 
 HB.factory Record DirLim_isFieldDirLim
-    (disp : unit) (I : dirType disp)
+    disp (I : dirType disp)
     (Obj : I -> fieldType)
     (bonding : forall i j, i <= j -> {rmorphism Obj i -> Obj j})
     (Sys : is_dirsys bonding)
   dlT of DirLim _ Sys dlT := {}.
 HB.builders Context
-    (disp : unit) (I : dirType disp)
+    disp (I : dirType disp)
     (Obj : I -> fieldType)
     (bonding : forall i j, i <= j -> {rmorphism Obj i -> Obj j})
     (Sys : is_dirsys bonding)
@@ -293,7 +291,7 @@ Open Scope quotient_scope.
 
 Section Implem.
 
-Variables (disp : unit) (I : dirType disp).
+Variables (disp : _) (I : dirType disp).
 Variable Obj : I -> choiceType.
 Variable bonding : forall i j, i <= j -> Obj i -> Obj j.
 Variable Sys : is_dirsys bonding.
@@ -309,7 +307,7 @@ Notation "{ 'dirlim' S }" := (dirlim S).
 
 Section DirectLimitTheory.
 
-Variables (disp : unit) (I : dirType disp).
+Variables (disp : _) (I : dirType disp).
 Variable Obj : I -> choiceType.
 Variable bonding : forall i j, i <= j -> Obj i -> Obj j.
 Variable Sys : is_dirsys bonding.
@@ -377,7 +375,7 @@ Open Scope ring_scope.
 
 Section Instances.
 
-Variables (disp : unit) (I : dirType disp).
+Variables (disp : _) (I : dirType disp).
 
 Section NModule.
 Variable Obj : I -> nmodType.
@@ -516,7 +514,7 @@ End Instances.
 
 Section TestComUnitAlg.
 Variable (R : comRingType).
-Variables (disp : unit) (I : dirType disp).
+Variables (disp : _) (I : dirType disp).
 Variable Obj : I -> comUnitAlgType R.
 Variable bonding : forall i j, (i <= j)%O -> {lrmorphism Obj i -> Obj j}.
 Variable Sys : is_dirsys bonding.
diff --git a/theories/fps/dirlim_constr.v b/theories/fps/dirlim_constr.v
index b3d2f72..62ab325 100644
--- a/theories/fps/dirlim_constr.v
+++ b/theories/fps/dirlim_constr.v
@@ -34,10 +34,10 @@ Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 
 Reserved Notation "{ 'dirlim' S }" (at level 0, format "{ 'dirlim'  S }").
-Reserved Notation "''inj_' i" (at level 8, i at level 2, format "''inj_' i").
-Reserved Notation "''inj[' T ']'" (at level 8).
-Reserved Notation "''inj[' T ']_' i" (at level 8, i at level 2).
-Reserved Notation "''ind[' T ']'" (at level 8).
+Reserved Notation "''inj_' i" (at level 0, i at level 2, format "''inj_' i").
+Reserved Notation "''inj[' T ']'" (at level 0).
+Reserved Notation "''inj[' T ']_' i" (at level 0, i at level 2).
+Reserved Notation "''ind[' T ']'" (at level 0).
 
 
 
@@ -47,7 +47,7 @@ Reserved Notation "''ind[' T ']'" (at level 8).
 (***************************************************************************)
 Section DirectSystem.
 
-Variables (disp : unit) (I : dirType disp).
+Variables (disp : _) (I : dirType disp).
 
 (** Objects and bonding morphisms of the direct system at left outside     *)
 (** the record below to allows the addition of more algebraic structure    *)
@@ -145,9 +145,8 @@ Open Scope ring_scope.
 
 #[key="dlT"]
 HB.mixin Record isDirLim
-    (disp : unit) (I : dirType disp)
-    (Obj : I -> Type)
-    (bonding : forall i j, i <= j -> Obj i -> Obj j)
+    disp (I : dirType disp)
+    (Obj : I -> Type) (bonding : forall i j, i <= j -> Obj i -> Obj j)
     (Sys : is_dirsys bonding)
   dlT of Choice dlT := {
     dirlim_inj i : Obj i -> dlT;
@@ -168,9 +167,8 @@ HB.mixin Record isDirLim
 
 #[short(type="dirLimType")]
 HB.structure Definition DirLim
-    (disp : unit) (I : dirType disp)
-    (Obj : I -> Type)
-    (bonding : forall i j, i <= j -> Obj i -> Obj j)
+    disp (I : dirType disp)
+    (Obj : I -> Type) (bonding : forall i j, i <= j -> Obj i -> Obj j)
     (Sys : is_dirsys bonding)
   := {
     dlT of isDirLim disp I Obj bonding Sys dlT
@@ -181,8 +179,8 @@ HB.structure Definition DirLim
 
 Section InternalTheory.
 
-Variables (disp : unit) (I : dirType disp).
-Variable Obj : I -> Type.
+Variables (disp : _) (I : dirType disp).
+Variables Obj : I -> Type.
 Variable bonding : forall i j, i <= j -> Obj i -> Obj j.
 Variable Sys : is_dirsys bonding.
 Variable dlT : dirLimType Sys.
@@ -213,7 +211,7 @@ Notation "''ind'" := ('ind[ _ ]).
 
 Section DirLimDirected.
 
-Variables (disp : unit) (I : dirType disp).
+Variables (disp : _) (I : dirType disp).
 Variable Obj : I -> choiceType.
 Variable bonding : forall i j, i <= j -> Obj i -> Obj j.
 Variable Sys : is_dirsys bonding.
@@ -266,7 +264,7 @@ End DirLimDirected.
 
 Section Is_DirsysCongr.
 
-Variables (disp : unit) (I : dirType disp).
+Variables (disp : _) (I : dirType disp).
 Variable Obj : I -> Type.
 Variable bonding : forall i j, i <= j -> Obj i -> Obj j.
 Variable Sys : is_dirsys bonding.
@@ -309,7 +307,7 @@ Arguments dsysequal {disp I Obj bonding} (Sys) (u v).
 
 #[key="dlT"]
 HB.mixin Record isNmoduleDirLim
-    (disp : unit) (I : dirType disp)
+    disp (I : dirType disp)
     (Obj : I -> nmodType)
     (bonding : forall i j, i <= j -> {additive Obj i -> Obj j})
     (Sys : is_dirsys bonding)
@@ -319,7 +317,7 @@ HB.mixin Record isNmoduleDirLim
   }.
 #[short(type="nmodDirLimType")]
 HB.structure Definition NmoduleDirLim
-    (disp : unit) (I : dirType disp)
+    disp (I : dirType disp)
     (Obj : I -> nmodType)
     (bonding : forall i j, i <= j -> {additive Obj i -> Obj j})
     (Sys : is_dirsys bonding)
@@ -331,7 +329,7 @@ HB.structure Definition NmoduleDirLim
 
 Section NmoduleDirLimTheory.
 
-Variables (disp : unit) (I : dirType disp).
+Variables (disp : _) (I : dirType disp).
 Variable Obj : I -> nmodType.
 Variable bonding : forall i j, i <= j -> {additive Obj i -> Obj j}.
 Variable Sys : is_dirsys bonding.
@@ -375,7 +373,7 @@ End NmoduleDirLimTheory.
 
 #[short(type="zmodDirLimType")]
 HB.structure Definition ZmoduleDirLim
-    (disp : unit) (I : dirType disp)
+    disp (I : dirType disp)
     (Obj : I -> zmodType)
     (bonding : forall i j, i <= j -> {additive Obj i -> Obj j})
     (Sys : is_dirsys bonding)
@@ -386,7 +384,7 @@ HB.structure Definition ZmoduleDirLim
 
 Section ZmoduleDirLimTheory.
 
-Variables (disp : unit) (I : dirType disp).
+Variables (disp : _) (I : dirType disp).
 Variable Obj : I -> zmodType.
 Variable bonding : forall i j, i <= j -> {additive Obj i -> Obj j}.
 Variable Sys : is_dirsys bonding.
@@ -413,7 +411,7 @@ End ZmoduleDirLimTheory.
 
 #[key="dlT"]
 HB.mixin Record isSemiRingDirLim
-    (disp : unit) (I : dirType disp)
+    disp (I : dirType disp)
     (Obj : I -> semiRingType)
     (bonding : forall i j, i <= j -> {rmorphism Obj i -> Obj j})
     (Sys : is_dirsys bonding)
@@ -423,7 +421,7 @@ HB.mixin Record isSemiRingDirLim
   }.
 #[short(type="semiRingDirLimType")]
 HB.structure Definition SemiRingDirLim
-    (disp : unit) (I : dirType disp)
+    disp (I : dirType disp)
     (Obj : I -> semiRingType)
     (bonding : forall i j, i <= j -> {rmorphism Obj i -> Obj j})
     (Sys : is_dirsys bonding)
@@ -435,7 +433,7 @@ HB.structure Definition SemiRingDirLim
 
 Section SemiRingDirLimTheory.
 
-Variables (disp : unit) (I : dirType disp).
+Variables (disp : _) (I : dirType disp).
 Variable Obj : I -> semiRingType.
 Variable bonding : forall i j, i <= j -> {rmorphism Obj i -> Obj j}.
 Variable Sys : is_dirsys bonding.
@@ -478,7 +476,7 @@ End SemiRingDirLimTheory.
 
 #[short(type="ringDirLimType")]
 HB.structure Definition RingDirLim
-    (disp : unit) (I : dirType disp)
+    disp (I : dirType disp)
     (Obj : I -> ringType)
     (bonding : forall i j, i <= j -> {rmorphism Obj i -> Obj j})
     (Sys : is_dirsys bonding)
@@ -489,7 +487,7 @@ HB.structure Definition RingDirLim
 
 #[short(type="comSemiRingDirLimType")]
 HB.structure Definition ComSemiRingDirLim
-    (disp : unit) (I : dirType disp)
+    disp (I : dirType disp)
     (Obj : I -> comSemiRingType)
     (bonding : forall i j, i <= j -> {rmorphism Obj i -> Obj j})
     (Sys : is_dirsys bonding)
@@ -500,7 +498,7 @@ HB.structure Definition ComSemiRingDirLim
 
 #[short(type="comRingDirLimType")]
 HB.structure Definition ComRingDirLim
-    (disp : unit) (I : dirType disp)
+    disp (I : dirType disp)
     (Obj : I -> comRingType)
     (bonding : forall i j, i <= j -> {rmorphism Obj i -> Obj j})
     (Sys : is_dirsys bonding)
@@ -512,7 +510,7 @@ HB.structure Definition ComRingDirLim
 
 #[short(type="unitRingDirLimType")]
 HB.structure Definition UnitRingDirLim
-    (disp : unit) (I : dirType disp)
+    disp (I : dirType disp)
     (Obj : I -> unitRingType)
     (bonding : forall i j, i <= j -> {rmorphism Obj i -> Obj j})
     (Sys : is_dirsys bonding)
@@ -524,7 +522,7 @@ HB.structure Definition UnitRingDirLim
 Section DirLimUnitRingTheory.
 
 Variables
-    (disp : unit) (I : dirType disp)
+    (disp : _) (I : dirType disp)
     (Obj : I -> unitRingType)
     (bonding : forall i j, i <= j -> {rmorphism Obj i -> Obj j})
     (Sys : is_dirsys bonding).
@@ -558,7 +556,7 @@ End  DirLimUnitRingTheory.
 
 #[short(type="comUnitRingDirLimType")]
 HB.structure Definition ComUnitRingDirLim
-    (disp : unit) (I : dirType disp)
+    disp (I : dirType disp)
     (Obj : I -> comUnitRingType)
     (bonding : forall i j, i <= j -> {rmorphism Obj i -> Obj j})
     (Sys : is_dirsys bonding)
@@ -570,7 +568,7 @@ HB.structure Definition ComUnitRingDirLim
 
 #[short(type="idomainDirLimType")]
 HB.structure Definition IDomainDirLim
-    (disp : unit) (I : dirType disp)
+    disp (I : dirType disp)
     (Obj : I -> idomainType)
     (bonding : forall i j, i <= j -> {rmorphism Obj i -> Obj j})
     (Sys : is_dirsys bonding)
@@ -582,7 +580,7 @@ HB.structure Definition IDomainDirLim
 
 #[short(type="fieldDirLimType")]
 HB.structure Definition FieldDirLim
-    (disp : unit) (I : dirType disp)
+    disp (I : dirType disp)
     (Obj : I -> fieldType)
     (bonding : forall i j, i <= j -> {rmorphism Obj i -> Obj j})
     (Sys : is_dirsys bonding)
@@ -595,7 +593,7 @@ HB.structure Definition FieldDirLim
 #[key="dlT"]
   HB.mixin Record isLmoduleDirLim
     (R : ringType)
-    (disp : unit) (I : dirType disp)
+    disp (I : dirType disp)
     (Obj : I -> lmodType R)
     (bonding : forall i j, i <= j -> {linear Obj i -> Obj j})
     (Sys : is_dirsys bonding)
@@ -607,7 +605,7 @@ HB.structure Definition FieldDirLim
 #[short(type="lmodDirLimType")]
 HB.structure Definition LmoduleDirLim
     (R : ringType)
-    (disp : unit) (I : dirType disp)
+    disp (I : dirType disp)
     (Obj : I -> lmodType R)
     (bonding : forall i j, i <= j -> {linear Obj i -> Obj j})
     (Sys : is_dirsys bonding)
@@ -620,7 +618,7 @@ HB.structure Definition LmoduleDirLim
 Section LmoduleDirLimTheory.
 
 Variable (R : ringType).
-Variables (disp : unit) (I : dirType disp).
+Variables (disp : _) (I : dirType disp).
 Variable Obj : I -> lmodType R.
 Variable bonding : forall i j, i <= j -> {linear Obj i -> Obj j}.
 Variable Sys : is_dirsys bonding.
@@ -651,7 +649,7 @@ End LmoduleDirLimTheory.
 #[short(type="lalgDirLimType")]
 HB.structure Definition LalgebraDirLim
     (R : ringType)
-    (disp : unit) (I : dirType disp)
+    disp (I : dirType disp)
     (Obj : I -> lalgType R)
     (bonding : forall i j, i <= j -> {lrmorphism Obj i -> Obj j})
     (Sys : is_dirsys bonding)
@@ -664,7 +662,7 @@ HB.structure Definition LalgebraDirLim
 Section LAlgebraDirLimTheory.
 
 Variable (R : ringType).
-Variables (disp : unit) (I : dirType disp).
+Variables (disp : _) (I : dirType disp).
 Variable Obj : I -> lalgType R.
 Variable bonding : forall i j, i <= j -> {lrmorphism Obj i -> Obj j}.
 Variable Sys : is_dirsys bonding.
@@ -690,7 +688,7 @@ End LAlgebraDirLimTheory.
 #[short(type="algDirLimType")]
 HB.structure Definition AlgebraDirLim
     (R : ringType)
-    (disp : unit) (I : dirType disp)
+    disp (I : dirType disp)
     (Obj : I -> algType R)
     (bonding : forall i j, i <= j -> {lrmorphism Obj i -> Obj j})
     (Sys : is_dirsys bonding)
@@ -705,7 +703,7 @@ HB.structure Definition AlgebraDirLim
 #[short(type="comAlgDirLimType")]
 HB.structure Definition ComAlgebraDirLim
     (R : ringType)
-    (disp : unit) (I : dirType disp)
+    disp (I : dirType disp)
     (Obj : I -> comAlgType R)
     (bonding : forall i j, i <= j -> {lrmorphism Obj i -> Obj j})
     (Sys : is_dirsys bonding)
@@ -718,7 +716,7 @@ HB.structure Definition ComAlgebraDirLim
 #[short(type="comAlgDirLimType")]
 HB.structure Definition UnitAlgebraDirLim
     (R : ringType)
-    (disp : unit) (I : dirType disp)
+    disp (I : dirType disp)
     (Obj : I -> unitAlgType R)
     (bonding : forall i j, i <= j -> {lrmorphism Obj i -> Obj j})
     (Sys : is_dirsys bonding)
@@ -730,7 +728,7 @@ HB.structure Definition UnitAlgebraDirLim
 
 HB.structure Definition ComUnitAlgebraDirLim
     (R : ringType)
-    (disp : unit) (I : dirType disp)
+    disp (I : dirType disp)
     (Obj : I -> comUnitAlgType R)
     (bonding : forall i j, i <= j -> {lrmorphism Obj i -> Obj j})
     (Sys : is_dirsys bonding)
@@ -751,13 +749,13 @@ HB.structure Definition ComUnitAlgebraDirLim
 (****************************************************************************)
 
 HB.factory Record DirLim_isNmoduleDirLim
-    (disp : unit) (I : dirType disp)
+    disp (I : dirType disp)
     (Obj : I -> nmodType)
     (bonding : forall i j, i <= j -> {additive Obj i -> Obj j})
     (Sys : is_dirsys bonding)
   dlT of DirLim _ Sys dlT := {}.
 HB.builders Context
-    (disp : unit) (I : dirType disp)
+    disp (I : dirType disp)
     (Obj : I -> nmodType)
     (bonding : forall i j, i <= j -> {additive Obj i -> Obj j})
     (Sys : is_dirsys bonding)
@@ -819,13 +817,13 @@ HB.end.
 
 
 HB.factory Record NmoduleDirLim_isZmoduleDirLim
-    (disp : unit) (I : dirType disp)
+    disp (I : dirType disp)
     (Obj : I -> zmodType)
     (bonding : forall i j, i <= j -> {additive Obj i -> Obj j})
     (Sys : is_dirsys bonding)
   dlT of NmoduleDirLim _ Sys dlT := {}.
 HB.builders Context
-    (disp : unit) (I : dirType disp)
+    disp (I : dirType disp)
     (Obj : I -> zmodType)
     (bonding : forall i j, i <= j -> {additive Obj i -> Obj j})
     (Sys : is_dirsys bonding)
@@ -857,13 +855,13 @@ Qed.
 HB.end.
 
 HB.factory Record DirLim_isZmoduleDirLim
-    (disp : unit) (I : dirType disp)
+    disp (I : dirType disp)
     (Obj : I -> zmodType)
     (bonding : forall i j, i <= j -> {additive Obj i -> Obj j})
     (Sys : is_dirsys bonding)
   dlT of DirLim _ Sys dlT := {}.
 HB.builders Context
-    (disp : unit) (I : dirType disp)
+    disp (I : dirType disp)
     (Obj : I -> zmodType)
     (bonding : forall i j, i <= j -> {additive Obj i -> Obj j})
     (Sys : is_dirsys bonding)
@@ -876,13 +874,13 @@ HB.end.
 
 
 HB.factory Record NmoduleDirLim_isSemiRingDirLim
-    (disp : unit) (I : dirType disp)
+    disp (I : dirType disp)
     (Obj : I -> semiRingType)
     (bonding : forall i j, i <= j -> {rmorphism Obj i -> Obj j})
     (Sys : is_dirsys bonding)
   dlT of NmoduleDirLim _ Sys dlT := {}.
 HB.builders Context
-    (disp : unit) (I : dirType disp)
+    disp (I : dirType disp)
     (Obj : I -> semiRingType)
     (bonding : forall i j, i <= j -> {rmorphism Obj i -> Obj j})
     (Sys : is_dirsys bonding)
@@ -971,13 +969,13 @@ HB.instance Definition _ :=
 HB.end.
 
 HB.factory Record DirLim_isSemiRingDirLim
-    (disp : unit) (I : dirType disp)
+    disp (I : dirType disp)
     (Obj : I -> semiRingType)
     (bonding : forall i j, i <= j -> {rmorphism Obj i -> Obj j})
     (Sys : is_dirsys bonding)
   dlT of DirLim _ Sys dlT := {}.
 HB.builders Context
-    (disp : unit) (I : dirType disp)
+    disp (I : dirType disp)
     (Obj : I -> semiRingType)
     (bonding : forall i j, i <= j -> {rmorphism Obj i -> Obj j})
     (Sys : is_dirsys bonding)
@@ -990,13 +988,13 @@ HB.end.
 
 
 HB.factory Record SemiRingDirLim_isRingDirLim
-    (disp : unit) (I : dirType disp)
+    disp (I : dirType disp)
     (Obj : I -> ringType)
     (bonding : forall i j, i <= j -> {rmorphism Obj i -> Obj j})
     (Sys : is_dirsys bonding)
   dlT of SemiRingDirLim _ Sys dlT := {}.
 HB.builders Context
-    (disp : unit) (I : dirType disp)
+    disp (I : dirType disp)
     (Obj : I -> ringType)
     (bonding : forall i j, i <= j -> {rmorphism Obj i -> Obj j})
     (Sys : is_dirsys bonding)
@@ -1007,13 +1005,13 @@ HB.end.
 
 
 HB.factory Record DirLim_isRingDirLim
-    (disp : unit) (I : dirType disp)
+    disp (I : dirType disp)
     (Obj : I -> ringType)
     (bonding : forall i j, i <= j -> {rmorphism Obj i -> Obj j})
     (Sys : is_dirsys bonding)
   dlT of DirLim _ Sys dlT := {}.
 HB.builders Context
-    (disp : unit) (I : dirType disp)
+    disp (I : dirType disp)
     (Obj : I -> ringType)
     (bonding : forall i j, i <= j -> {rmorphism Obj i -> Obj j})
     (Sys : is_dirsys bonding)
@@ -1026,13 +1024,13 @@ HB.end.
 
 
 HB.factory Record SemiRingDirLim_isComSemiRingDirLim
-    (disp : unit) (I : dirType disp)
+    disp (I : dirType disp)
     (Obj : I -> comSemiRingType)
     (bonding : forall i j, i <= j -> {rmorphism Obj i -> Obj j})
     (Sys : is_dirsys bonding)
   dlT of SemiRingDirLim _ Sys dlT := {}.
 HB.builders Context
-    (disp : unit) (I : dirType disp)
+    disp (I : dirType disp)
     (Obj : I -> comSemiRingType)
     (bonding : forall i j, i <= j -> {rmorphism Obj i -> Obj j})
     (Sys : is_dirsys bonding)
@@ -1052,13 +1050,13 @@ HB.end.
 
 
 HB.factory Record DirLim_isComSemiRingDirLim
-    (disp : unit) (I : dirType disp)
+    disp (I : dirType disp)
     (Obj : I -> comSemiRingType)
     (bonding : forall i j, i <= j -> {rmorphism Obj i -> Obj j})
     (Sys : is_dirsys bonding)
   dlT of DirLim _ Sys dlT := {}.
 HB.builders Context
-    (disp : unit) (I : dirType disp)
+    disp (I : dirType disp)
     (Obj : I -> comSemiRingType)
     (bonding : forall i j, i <= j -> {rmorphism Obj i -> Obj j})
     (Sys : is_dirsys bonding)
@@ -1071,13 +1069,13 @@ HB.end.
 
 
 HB.factory Record RingDirLim_isComRingDirLim
-    (disp : unit) (I : dirType disp)
+    disp (I : dirType disp)
     (Obj : I -> comRingType)
     (bonding : forall i j, i <= j -> {rmorphism Obj i -> Obj j})
     (Sys : is_dirsys bonding)
   dlT of RingDirLim _ Sys dlT := {}.
 HB.builders Context
-    (disp : unit) (I : dirType disp)
+    disp (I : dirType disp)
     (Obj : I -> comRingType)
     (bonding : forall i j, i <= j -> {rmorphism Obj i -> Obj j})
     (Sys : is_dirsys bonding)
@@ -1088,13 +1086,13 @@ HB.end.
 
 
 HB.factory Record DirLim_isComRingDirLim
-    (disp : unit) (I : dirType disp)
+    disp (I : dirType disp)
     (Obj : I -> comRingType)
     (bonding : forall i j, i <= j -> {rmorphism Obj i -> Obj j})
     (Sys : is_dirsys bonding)
   dlT of DirLim _ Sys dlT := {}.
 HB.builders Context
-    (disp : unit) (I : dirType disp)
+    disp (I : dirType disp)
     (Obj : I -> comRingType)
     (bonding : forall i j, i <= j -> {rmorphism Obj i -> Obj j})
     (Sys : is_dirsys bonding)
@@ -1107,7 +1105,7 @@ HB.end.
 
 
 HB.factory Record RingDirLim_isUnitRingDirLim
-    (disp : unit) (I : dirType disp)
+    disp (I : dirType disp)
     (Obj : I -> unitRingType)
     (bonding : forall i j, i <= j -> {rmorphism Obj i -> Obj j})
     (Sys : is_dirsys bonding)
@@ -1118,7 +1116,7 @@ HB.factory Record RingDirLim_isUnitRingDirLim
         (dlunit x)
   }.
 HB.builders Context
-    (disp : unit) (I : dirType disp)
+    disp (I : dirType disp)
     (Obj : I -> unitRingType)
     (bonding : forall i j, i <= j -> {rmorphism Obj i -> Obj j})
     (Sys : is_dirsys bonding)
@@ -1187,13 +1185,13 @@ HB.end.
 
 
 HB.factory Record UnitRingDirLim_isComUnitRingDirLim
-    (disp : unit) (I : dirType disp)
+    disp (I : dirType disp)
     (Obj : I -> comUnitRingType)
     (bonding : forall i j, i <= j -> {rmorphism Obj i -> Obj j})
     (Sys : is_dirsys bonding)
   dlT of UnitRingDirLim _ Sys dlT := {}.
 HB.builders Context
-    (disp : unit) (I : dirType disp)
+    disp (I : dirType disp)
     (Obj : I -> comUnitRingType)
     (bonding : forall i j, i <= j -> {rmorphism Obj i -> Obj j})
     (Sys : is_dirsys bonding)
@@ -1208,13 +1206,13 @@ HB.end.
 
 
 HB.factory Record ComUnitRingDirLim_isIntegralDirLim
-    (disp : unit) (I : dirType disp)
+    disp (I : dirType disp)
     (Obj : I -> idomainType)
     (bonding : forall i j, i <= j -> {rmorphism Obj i -> Obj j})
     (Sys : is_dirsys bonding)
   dlT of ComUnitRingDirLim _ Sys dlT := {}.
 HB.builders Context
-    (disp : unit) (I : dirType disp)
+    disp (I : dirType disp)
     (Obj : I -> idomainType)
     (bonding : forall i j, i <= j -> {rmorphism Obj i -> Obj j})
     (Sys : is_dirsys bonding)
@@ -1238,13 +1236,13 @@ HB.end.
 
 
 HB.factory Record IDomainDirLim_isFieldDirLim
-    (disp : unit) (I : dirType disp)
+    disp (I : dirType disp)
     (Obj : I -> fieldType)
     (bonding : forall i j, i <= j -> {rmorphism Obj i -> Obj j})
     (Sys : is_dirsys bonding)
   dlT of IDomainDirLim _ Sys dlT := {}.
 HB.builders Context
-    (disp : unit) (I : dirType disp)
+    disp (I : dirType disp)
     (Obj : I -> fieldType)
     (bonding : forall i j, i <= j -> {rmorphism Obj i -> Obj j})
     (Sys : is_dirsys bonding)
@@ -1265,14 +1263,14 @@ HB.end.
 
 HB.factory Record ZmoduleDirLim_isLmoduleDirLim
     (R : ringType)
-    (disp : unit) (I : dirType disp)
+    disp (I : dirType disp)
     (Obj : I -> lmodType R)
     (bonding : forall i j, i <= j -> {linear Obj i -> Obj j})
     (Sys : is_dirsys bonding)
   dlT of ZmoduleDirLim _ Sys dlT := {}.
 HB.builders Context
     (R : ringType)
-    (disp : unit) (I : dirType disp)
+    disp (I : dirType disp)
     (Obj : I -> lmodType R)
     (bonding : forall i j, i <= j -> {linear Obj i -> Obj j})
     (Sys : is_dirsys bonding)
@@ -1326,14 +1324,14 @@ HB.end.
 
 HB.factory Record DirLim_isLmoduleDirLim
     (R : ringType)
-    (disp : unit) (I : dirType disp)
+    disp (I : dirType disp)
     (Obj : I -> lmodType R)
     (bonding : forall i j, i <= j -> {linear Obj i -> Obj j})
     (Sys : is_dirsys bonding)
   dlT of DirLim _ Sys dlT := {}.
 HB.builders Context
     (R : ringType)
-    (disp : unit) (I : dirType disp)
+    disp (I : dirType disp)
     (Obj : I -> lmodType R)
     (bonding : forall i j, i <= j -> {linear Obj i -> Obj j})
     (Sys : is_dirsys bonding)
@@ -1347,14 +1345,14 @@ HB.end.
 
 HB.factory Record LmoduleDirLim_isLalgebraDirLim
     (R : ringType)
-    (disp : unit) (I : dirType disp)
+    disp (I : dirType disp)
     (Obj : I -> lalgType R)
     (bonding : forall i j, i <= j -> {lrmorphism Obj i -> Obj j})
     (Sys : is_dirsys bonding)
   dlT of LmoduleDirLim _ Sys dlT := {}.
 HB.builders Context
     (R : ringType)
-    (disp : unit) (I : dirType disp)
+    disp (I : dirType disp)
     (Obj : I -> lalgType R)
     (bonding : forall i j, i <= j -> {lrmorphism Obj i -> Obj j})
     (Sys : is_dirsys bonding)
@@ -1378,14 +1376,14 @@ HB.end.
 
 HB.factory Record DirLim_isLalgebraDirLim
     (R : ringType)
-    (disp : unit) (I : dirType disp)
+    disp (I : dirType disp)
     (Obj : I -> lalgType R)
     (bonding : forall i j, i <= j -> {lrmorphism Obj i -> Obj j})
     (Sys : is_dirsys bonding)
   dlT of DirLim _ Sys dlT := {}.
 HB.builders Context
     (R : ringType)
-    (disp : unit) (I : dirType disp)
+    disp (I : dirType disp)
     (Obj : I -> lalgType R)
     (bonding : forall i j, i <= j -> {lrmorphism Obj i -> Obj j})
     (Sys : is_dirsys bonding)
@@ -1400,14 +1398,14 @@ HB.end.
 
 HB.factory Record LalgebraDirLim_isAlgebraDirLim
     (R : comRingType)
-    (disp : unit) (I : dirType disp)
+    disp (I : dirType disp)
     (Obj : I -> algType R)
     (bonding : forall i j, i <= j -> {lrmorphism Obj i -> Obj j})
     (Sys : is_dirsys bonding)
   dlT of LalgebraDirLim _ Sys dlT := {}.
 HB.builders Context
     (R : comRingType)
-    (disp : unit) (I : dirType disp)
+    disp (I : dirType disp)
     (Obj : I -> algType R)
     (bonding : forall i j, i <= j -> {lrmorphism Obj i -> Obj j})
     (Sys : is_dirsys bonding)
@@ -1428,14 +1426,14 @@ HB.end.
 
 HB.factory Record DirLim_isAlgebraDirLim
     (R : comRingType)
-    (disp : unit) (I : dirType disp)
+    disp (I : dirType disp)
     (Obj : I -> algType R)
     (bonding : forall i j, i <= j -> {lrmorphism Obj i -> Obj j})
     (Sys : is_dirsys bonding)
   dlT of DirLim _ Sys dlT := {}.
 HB.builders Context
     (R : comRingType)
-    (disp : unit) (I : dirType disp)
+    disp (I : dirType disp)
     (Obj : I -> algType R)
     (bonding : forall i j, i <= j -> {lrmorphism Obj i -> Obj j})
     (Sys : is_dirsys bonding)
diff --git a/theories/fps/fps.v b/theories/fps/fps.v
index ca25553..a337c55 100644
--- a/theories/fps/fps.v
+++ b/theories/fps/fps.v
@@ -96,7 +96,8 @@ We prove the [Lagrange_Bürmann] theorem giving the coefficent of the Lagrange
 fixpoint and its compose series.
 *******************************************************************************)
 From HB Require Import structures.
-From mathcomp Require Import all_ssreflect all_algebra.
+From mathcomp Require Import all_ssreflect.
+From mathcomp Require Import ssralg poly ring_quotient (* avoid sesquilinear *).
 From mathcomp Require Import boolp classical_sets.
 From mathcomp Require Import order.
 
@@ -114,14 +115,15 @@ Local Open Scope ring_scope.
 
 Declare Scope fps_scope.
 Delimit Scope fps_scope with fps.
+Local Open Scope fps_scope.
 
 Reserved Notation "{ 'fps' R }"
          (at level 0, R at level 2, format "{ 'fps'  R }").
-Reserved Notation "c %:S" (at level 2, format "c %:S").
+Reserved Notation "c %:S" (at level 1, format "c %:S").
 Reserved Notation "\fps E .X^ i"
   (at level 36, E at level 36, i at level 50, format "\fps  E  .X^ i").
 Reserved Notation "''X" (at level 0).
-Reserved Notation "a ^`` ()" (at level 8, format "a ^`` ()").
+Reserved Notation "a ^`` ()" (at level 1, format "a ^`` ()").
 Reserved Notation "s ``_ i" (at level 3, i at level 2, left associativity,
                             format "s ``_ i").
 Reserved Notation "f \oS g" (at level 50).
@@ -261,7 +263,7 @@ Section CoeffSeries.
 
 Variable R : ringType.
 
-Implicit Types (a b c: R) (s t u : {fps R}) (p q : {poly R}) (i j : nat).
+Implicit Types (a b c : R) (s t u : {fps R}) (p q : {poly R}) (i j : nat).
 
 Lemma proj0 i : 'pi[{fps R}]_i 0 = 0.
 Proof. exact: raddf0. Qed.
@@ -330,6 +332,7 @@ Proof. by move=> s t; rewrite /= !coefs_projE projB coefB. Qed.
 HB.instance Definition _ i :=
   GRing.isAdditive.Build {fps R} R _ (coefs_is_additive i).
 
+
 Lemma coefsD s t i : (s + t)``_i = s``_i + t``_i.
 Proof. exact: (raddfD (coefs i)). Qed.
 Lemma coefsN s i : (- s)``_i = - (s``_i).
@@ -604,7 +607,6 @@ Section FpsUnitRing.
 Variable R : unitRingType.
 Implicit Type f : {fps R}.
 
-HB.instance Definition _ := RingInvLim.on {fps R}.
 HB.instance Definition _ :=
   InvLim_isUnitRingInvLim.Build _ _ _ _ _ {fps R}.
 
diff --git a/theories/fps/invlim.v b/theories/fps/invlim.v
index b7bb181..820d9a9 100644
--- a/theories/fps/invlim.v
+++ b/theories/fps/invlim.v
@@ -37,7 +37,7 @@ Reserved Notation "{ 'invlim' S }"
          (at level 0, format "{ 'invlim'  S }").
 Reserved Notation "''pi_' i" (at level 8, i at level 2, format "''pi_' i").
 Reserved Notation "''pi[' T ']_' i" (at level 8, i at level 2).
-Reserved Notation "''ind[' T ']'" (at level 8).
+Reserved Notation "''ind[' T ']'" (at level 0).
 
 Reserved Notation "\Sum_( i : t ) F"
          (at level 41, F at level 41, i at level 50,
@@ -53,7 +53,7 @@ Reserved Notation "\Sum_( i ) F"
 (***************************************************************************)
 Section InverseSystem.
 
-Variables (disp : unit) (I : porderType disp).
+Variables (disp : _) (I : porderType disp).
 
 (** Objects and bonding morphisms of the inverse system at left outside    *)
 (** the record below to allows the addition of more algebraic structure    *)
@@ -95,11 +95,8 @@ Open Scope ring_scope.
 
 
 #[key="ilT"]
-HB.mixin Record isInvLim
-    (disp : unit) (I : porderType disp)
-    (Obj : I -> Type)
-    (bonding : forall i j, i <= j -> Obj j -> Obj i)
-    (Sys : is_invsys bonding)
+HB.mixin Record isInvLim disp (I : porderType disp) (Obj : I -> Type)
+    (bonding : forall i j, i <= j -> Obj j -> Obj i) (Sys : is_invsys bonding)
   ilT of Choice ilT := {
     invlim_proj : forall i, ilT -> Obj i;
     invlim_ind  : forall (T : Type) (f : forall i, T -> Obj i),
@@ -114,11 +111,8 @@ HB.mixin Record isInvLim
   }.
 
 #[short(type="invLimType")]
-HB.structure Definition InvLim
-    (disp : unit) (I : porderType disp)
-    (Obj : I -> Type)
-    (bonding : forall i j, i <= j -> Obj j -> Obj i)
-    (Sys : is_invsys bonding)
+HB.structure Definition InvLim disp (I : porderType disp) (Obj : I -> Type)
+    (bonding : forall i j, i <= j -> Obj j -> Obj i) (Sys : is_invsys bonding)
   := {
     ilT of isInvLim disp I Obj bonding Sys ilT
     & Choice ilT
@@ -128,11 +122,9 @@ HB.structure Definition InvLim
 
 Section InternalTheory.
 
-Variables (disp : unit) (I : porderType disp).
-Variable Obj : I -> Type.
-Variable bonding : forall i j, i <= j -> Obj j -> Obj i.
-Variable Sys : is_invsys bonding.
-Variable ilT : invLimType Sys.
+Variables (disp : _) (I : porderType disp).
+Variables (Obj : I -> Type) (bonding : forall i j, i <= j -> Obj j -> Obj i).
+Variables (Sys : is_invsys bonding) (ilT : invLimType Sys).
 
 Local Notation "\pi" := (invlim_proj (s := ilT)).
 Local Notation "\ind" := (invlim_ind (s := ilT) _ _).
@@ -157,11 +149,9 @@ Notation "''ind'" := ('ind[ _ ]).
 
 Section Theory.
 
-Variables (disp : unit) (I : porderType disp).
-Variable Obj : I -> Type.
-Variable bonding : forall i j, i <= j -> Obj j -> Obj i.
-Variable Sys : is_invsys bonding.
-Variable ilT : invLimType Sys.
+Variables (disp : _) (I : porderType disp).
+Variables (Obj : I -> Type) (bonding : forall i j, i <= j -> Obj j -> Obj i).
+Variables (Sys : is_invsys bonding) (ilT : invLimType Sys).
 
 Lemma invlimE (x y : ilT) : (forall i, 'pi_i x = 'pi_i y) -> x = y.
 Proof.
@@ -204,11 +194,9 @@ Arguments ilthr {disp I Obj bonding Sys ilT thr}.
 
 Section InvLimitDirected.
 
-Variables (disp : unit) (I : dirType disp).
-Variable Obj : I -> Type.
-Variable bonding : forall i j, i <= j -> Obj j -> Obj i.
-Variable Sys : is_invsys bonding.
-Variable ilT : invLimType Sys.
+Variables (disp : _) (I : dirType disp).
+Variables (Obj : I -> Type) (bonding : forall i j, i <= j -> Obj j -> Obj i).
+Variables (Sys : is_invsys bonding) (ilT : invLimType Sys).
 
 Lemma invlim_geE b (x y : ilT) :
   (forall i, i >= b -> 'pi_i x = 'pi_i y) -> x = y.
@@ -223,12 +211,10 @@ Arguments invlim_geE {disp I Obj bonding Sys ilT}.
 
 Section InvLimitEqType.
 
-Variables (disp : unit) (I : porderType disp).
-Variable Obj : I -> eqType.
-Variable bonding : forall i j, i <= j -> Obj j -> Obj i.
+Variables (disp : _) (I : porderType disp).
+Variables (Obj : I -> eqType) (bonding : forall i j, i <= j -> Obj j -> Obj i).
+Variables (Sys : is_invsys bonding) (ilT : invLimType Sys).
 
-Variable Sys : is_invsys bonding.
-Variable ilT : invLimType Sys.
 Implicit Type x y : ilT.
 
 Lemma invlimPn x y : reflect (exists i, 'pi_i x != 'pi_i y) (x != y).
@@ -272,9 +258,7 @@ End InvLimitEqType.
 (****************************************************************************)
 
 #[key="ilT"]
-HB.mixin Record isNmoduleInvLim
-    (disp : unit) (I : porderType disp)
-    (Obj : I -> nmodType)
+HB.mixin Record isNmoduleInvLim disp (I : porderType disp) (Obj : I -> nmodType)
     (bonding : forall i j, i <= j -> {additive Obj j -> Obj i})
     (Sys : is_invsys bonding)
     (ilT : Type) of InvLim disp Sys ilT & GRing.Nmodule ilT := {
@@ -283,7 +267,7 @@ HB.mixin Record isNmoduleInvLim
   }.
 #[short(type="nmodInvLimType")]
 HB.structure Definition NmodInvLim
-    (disp : unit) (I : porderType disp)
+    disp (I : porderType disp)
     (Obj : I -> nmodType)
     (bonding : forall i j, i <= j -> {additive Obj j -> Obj i})
     (Sys : is_invsys bonding)
@@ -295,12 +279,11 @@ HB.structure Definition NmodInvLim
 
 Section NmodInvLimTheory.
 
-Variables (disp : unit) (I : porderType disp).
+Variables (disp : _) (I : porderType disp).
 Variable Obj : I -> nmodType.
 Variable bonding : forall i j, i <= j -> {additive Obj j -> Obj i}.
-Variable Sys : is_invsys bonding.
+Variables (Sys : is_invsys bonding) (ilT : nmodInvLimType Sys).
 
-Variable ilT : nmodInvLimType Sys.
 Implicit Type x y : ilT.
 
 #[export] HB.instance Definition _ i :=
@@ -329,8 +312,7 @@ End NmodInvLimTheory.
 
 #[short(type="zmodInvLimType")]
 HB.structure Definition ZmodInvLim
-    (disp : unit) (I : porderType disp)
-    (Obj : I -> nmodType)
+    disp (I : porderType disp) (Obj : I -> nmodType)
     (bonding : forall i j, i <= j -> {additive Obj j -> Obj i})
     (Sys : is_invsys bonding)
   := {
@@ -340,7 +322,7 @@ HB.structure Definition ZmodInvLim
 
 Section ZmodInvLimTheory.
 
-Variables (disp : unit) (I : porderType disp).
+Variables (disp : _) (I : porderType disp).
 Variable Obj : I -> zmodType.
 Variable bonding : forall i j, i <= j -> {additive Obj j -> Obj i}.
 Variable Sys : is_invsys bonding.
@@ -356,16 +338,17 @@ Hypothesis Hcone : cone Sys f.
 
 Fact ilind_is_additive : additive ('ind[ilT] Hcone).
 Proof. exact: raddfB. Qed.
+(* Already instance of semi-additive
 #[export] HB.instance Definition _ :=
   GRing.isAdditive.Build T ilT _ ilind_is_additive.
-
+*)
 End UniversalProperty.
 End ZmodInvLimTheory.
 
 
 #[key="ilT"]
 HB.mixin Record isSemiRingInvLim
-    (disp : unit) (I : porderType disp)
+    disp (I : porderType disp)
     (Obj : I -> semiRingType)
     (bonding : forall i j, i <= j -> {rmorphism Obj j -> Obj i})
     (Sys : is_invsys bonding)
@@ -375,7 +358,7 @@ HB.mixin Record isSemiRingInvLim
   }.
 #[short(type="semiRingInvLimType")]
 HB.structure Definition SemiRingInvLim
-    (disp : unit) (I : porderType disp)
+    disp (I : porderType disp)
     (Obj : I -> semiRingType)
     (bonding : forall i j, i <= j -> {rmorphism Obj j -> Obj i})
     (Sys : is_invsys bonding)
@@ -387,7 +370,7 @@ HB.structure Definition SemiRingInvLim
 
 Section SemiRingInvLimTheory.
 
-Variables (disp : unit) (I : porderType disp).
+Variables (disp : _) (I : porderType disp).
 Variable Obj : I -> semiRingType.
 Variable bonding : forall i j, i <= j -> {rmorphism Obj j -> Obj i}.
 Variable Sys : is_invsys bonding.
@@ -421,7 +404,7 @@ End SemiRingInvLimTheory.
 
 #[short(type="ringInvLimType")]
 HB.structure Definition RingInvLim
-    (disp : unit) (I : porderType disp)
+    disp (I : porderType disp)
     (Obj : I -> semiRingType)
     (bonding : forall i j, i <= j -> {rmorphism Obj j -> Obj i})
     (Sys : is_invsys bonding)
@@ -433,7 +416,7 @@ HB.structure Definition RingInvLim
 
 #[short(type="comSemiRingInvLimType")]
 HB.structure Definition ComSemiRingInvLim
-    (disp : unit) (I : porderType disp)
+    disp (I : porderType disp)
     (Obj : I -> semiRingType)
     (bonding : forall i j, i <= j -> {rmorphism Obj j -> Obj i})
     (Sys : is_invsys bonding)
@@ -445,7 +428,7 @@ HB.structure Definition ComSemiRingInvLim
 
 #[short(type="comRingInvLimType")]
 HB.structure Definition ComRingInvLim
-    (disp : unit) (I : porderType disp)
+    disp (I : porderType disp)
     (Obj : I -> semiRingType)
     (bonding : forall i j, i <= j -> {rmorphism Obj j -> Obj i})
     (Sys : is_invsys bonding)
@@ -457,7 +440,7 @@ HB.structure Definition ComRingInvLim
 
 #[short(type="unitRingInvLimType")]
 HB.structure Definition UnitRingInvLim
-    (disp : unit) (I : porderType disp)
+    disp (I : porderType disp)
     (Obj : I -> semiRingType)
     (bonding : forall i j, i <= j -> {rmorphism Obj j -> Obj i})
     (Sys : is_invsys bonding)
@@ -469,7 +452,7 @@ HB.structure Definition UnitRingInvLim
 Section InvLimUnitRingTheory.
 
 Variables
-    (disp : unit) (I : porderType disp)
+    (disp : _) (I : porderType disp)
     (Obj : I -> unitRingType)
     (bonding : forall i j, i <= j -> {rmorphism Obj j -> Obj i})
     (Sys : is_invsys bonding).
@@ -493,7 +476,7 @@ End  InvLimUnitRingTheory.
 
 #[short(type="comUnitRingInvLimType")]
 HB.structure Definition ComUnitRingInvLim
-    (disp : unit) (I : porderType disp)
+    disp (I : porderType disp)
     (Obj : I -> semiRingType)
     (bonding : forall i j, i <= j -> {rmorphism Obj j -> Obj i})
     (Sys : is_invsys bonding)
@@ -505,7 +488,7 @@ HB.structure Definition ComUnitRingInvLim
 
 #[short(type="idomainInvLimType")]
 HB.structure Definition IDomainInvLim
-    (disp : unit) (I : porderType disp)
+    disp (I : porderType disp)
     (Obj : I -> semiRingType)
     (bonding : forall i j, i <= j -> {rmorphism Obj j -> Obj i})
     (Sys : is_invsys bonding)
@@ -517,7 +500,7 @@ HB.structure Definition IDomainInvLim
 
 #[short(type="fieldInvLimType")]
 HB.structure Definition FieldRingInvLim
-    (disp : unit) (I : porderType disp)
+    disp (I : porderType disp)
     (Obj : I -> semiRingType)
     (bonding : forall i j, i <= j -> {rmorphism Obj j -> Obj i})
     (Sys : is_invsys bonding)
@@ -530,7 +513,7 @@ HB.structure Definition FieldRingInvLim
 #[key="ilT"]
 HB.mixin Record isLmodInvLim
     (R : ringType)
-    (disp : unit) (I : porderType disp)
+    disp (I : porderType disp)
     (Obj : I -> lmodType R)
     (bonding : forall i j, i <= j -> {linear Obj j -> Obj i})
     (Sys : is_invsys bonding)
@@ -541,7 +524,7 @@ HB.mixin Record isLmodInvLim
 #[short(type="lmodInvLimType")]
 HB.structure Definition LmodInvLim
     (R : ringType)
-    (disp : unit) (I : porderType disp)
+    disp (I : porderType disp)
     (Obj : I -> lmodType R)
     (bonding : forall i j, i <= j -> {linear Obj j -> Obj i})
     (Sys : is_invsys bonding)
@@ -554,7 +537,7 @@ HB.structure Definition LmodInvLim
 Section LmodInvLimTheory.
 
 Variable (R : ringType).
-Variables (disp : unit) (I : porderType disp).
+Variables (disp : _) (I : porderType disp).
 Variable Obj : I -> lmodType R.
 Variable bonding : forall i j, i <= j -> {linear Obj j -> Obj i}.
 Variable Sys : is_invsys bonding.
@@ -585,7 +568,7 @@ End LmodInvLimTheory.
 #[short(type="lalgInvLimType")]
 HB.structure Definition LalgebraInvLim
     (R : ringType)
-    (disp : unit) (I : porderType disp)
+    disp (I : porderType disp)
     (Obj : I -> lalgType R)
     (bonding : forall i j, i <= j -> {lrmorphism Obj j -> Obj i})
     (Sys : is_invsys bonding)
@@ -598,7 +581,7 @@ HB.structure Definition LalgebraInvLim
 Section LAlgInvLimTheory.
 
 Variable (R : ringType).
-Variables (disp : unit) (I : porderType disp).
+Variables (disp : _) (I : porderType disp).
 Variable Obj : I -> lalgType R.
 Variable bonding : forall i j, i <= j -> {lrmorphism Obj j -> Obj i}.
 Variable Sys : is_invsys bonding.
@@ -624,7 +607,7 @@ End LAlgInvLimTheory.
 #[short(type="algInvLimType")]
 HB.structure Definition AlgebraInvLim
     (R : ringType)
-    (disp : unit) (I : porderType disp)
+    disp (I : porderType disp)
     (Obj : I -> lalgType R)
     (bonding : forall i j, i <= j -> {lrmorphism Obj j -> Obj i})
     (Sys : is_invsys bonding)
@@ -646,13 +629,13 @@ HB.structure Definition AlgebraInvLim
 
 
 HB.factory Record InvLim_isNmodInvLim
-    (disp : unit) (I : porderType disp)
+    disp (I : porderType disp)
     (Obj : I -> nmodType)
     (bonding : forall i j, i <= j -> {additive Obj j -> Obj i})
     (Sys : is_invsys bonding)
   ilT of InvLim _ Sys ilT := {}.
 HB.builders Context
-    (disp : unit) (I : porderType disp)
+    disp (I : porderType disp)
     (Obj : I -> nmodType)
     (bonding : forall i j, i <= j -> {additive Obj j -> Obj i})
     (Sys : is_invsys bonding)
@@ -686,13 +669,13 @@ HB.end.
 
 
 HB.factory Record InvLim_isZmodInvLim
-    (disp : unit) (I : porderType disp)
+    disp (I : porderType disp)
     (Obj : I -> zmodType)
     (bonding : forall i j, i <= j -> {additive Obj j -> Obj i})
     (Sys : is_invsys bonding)
   ilT of InvLim _ Sys ilT := {}.
 HB.builders Context
-    (disp : unit) (I : porderType disp)
+    disp (I : porderType disp)
     (Obj : I -> zmodType)
     (bonding : forall i j, i <= j -> {additive Obj j -> Obj i})
     (Sys : is_invsys bonding)
@@ -715,13 +698,13 @@ HB.end.
 
 
 HB.factory Record InvLim_isSemiRingInvLim
-    (disp : unit) (I : porderType disp)
+    disp (I : porderType disp)
     (Obj : I -> semiRingType)
     (bonding : forall i j, i <= j -> {rmorphism Obj j -> Obj i})
     (Sys : is_invsys bonding)
   ilT of InvLim _ Sys ilT := {}.
 HB.builders Context
-    (disp : unit) (I : porderType disp)
+    disp (I : porderType disp)
     (Obj : I -> semiRingType)
     (bonding : forall i j, i <= j -> {rmorphism Obj j -> Obj i})
     (Sys : is_invsys bonding)
@@ -772,13 +755,13 @@ HB.end.
 
 
 HB.factory Record InvLim_isRingInvLim
-    (disp : unit) (I : porderType disp)
+    disp (I : porderType disp)
     (Obj : I -> ringType)
     (bonding : forall i j, i <= j -> {rmorphism Obj j -> Obj i})
     (Sys : is_invsys bonding)
   ilT of InvLim _ Sys ilT := {}.
 HB.builders Context
-    (disp : unit) (I : porderType disp)
+    disp (I : porderType disp)
     (Obj : I -> ringType)
     (bonding : forall i j, i <= j -> {rmorphism Obj j -> Obj i})
     (Sys : is_invsys bonding)
@@ -793,13 +776,13 @@ HB.end.
 
 
 HB.factory Record InvLim_isComSemiRingInvLim
-    (disp : unit) (I : porderType disp)
+    disp (I : porderType disp)
     (Obj : I -> comSemiRingType)
     (bonding : forall i j, i <= j -> {rmorphism Obj j -> Obj i})
     (Sys : is_invsys bonding)
   ilT of InvLim _ Sys ilT := {}.
 HB.builders Context
-    (disp : unit) (I : porderType disp)
+    disp (I : porderType disp)
     (Obj : I -> comSemiRingType)
     (bonding : forall i j, i <= j -> {rmorphism Obj j -> Obj i})
     (Sys : is_invsys bonding)
@@ -822,13 +805,13 @@ HB.end.
 
 
 HB.factory Record InvLim_isUnitRingInvLim
-    (disp : unit) (I : porderType disp)
+    disp (I : porderType disp)
     (Obj : I -> unitRingType)
     (bonding : forall i j, i <= j -> {rmorphism Obj j -> Obj i})
     (Sys : is_invsys bonding)
   ilT of InvLim _ Sys ilT := {}.
 HB.builders Context
-    (disp : unit) (I : porderType disp)
+    disp (I : porderType disp)
     (Obj : I -> unitRingType)
     (bonding : forall i j, i <= j -> {rmorphism Obj j -> Obj i})
     (Sys : is_invsys bonding)
@@ -882,13 +865,13 @@ HB.end.
 
 
 HB.factory Record InvLim_isIDomainInvLim
-    (disp : unit) (I : dirType disp)
+    disp (I : dirType disp)
     (Obj : I -> idomainType)
     (bonding : forall i j, i <= j -> {rmorphism Obj j -> Obj i})
     (Sys : is_invsys bonding)
   ilT of InvLim _ Sys ilT := {}.
 HB.builders Context
-    (disp : unit) (I : dirType disp)
+    disp (I : dirType disp)
     (Obj : I -> idomainType)
     (bonding : forall i j, i <= j -> {rmorphism Obj j -> Obj i})
     (Sys : is_invsys bonding)
@@ -922,13 +905,13 @@ HB.end.
 
 
 HB.factory Record InvLim_isFieldInvLim
-    (disp : unit) (I : dirType disp)
+    disp (I : dirType disp)
     (Obj : I -> fieldType)
     (bonding : forall i j, i <= j -> {rmorphism Obj j -> Obj i})
     (Sys : is_invsys bonding)
   ilT of InvLim _ Sys ilT := {}.
 HB.builders Context
-    (disp : unit) (I : dirType disp)
+    disp (I : dirType disp)
     (Obj : I -> fieldType)
     (bonding : forall i j, i <= j -> {rmorphism Obj j -> Obj i})
     (Sys : is_invsys bonding)
@@ -955,14 +938,14 @@ HB.end.
 
 HB.factory Record InvLim_isLmoduleInvLim
     (R : ringType)
-    (disp : unit) (I : porderType disp)
+    disp (I : porderType disp)
     (Obj : I -> lmodType R)
     (bonding : forall i j, i <= j -> {linear Obj j -> Obj i})
     (Sys : is_invsys bonding)
   ilT of InvLim _ Sys ilT := {}.
 HB.builders Context
     (R : ringType)
-    (disp : unit) (I : porderType disp)
+    disp (I : porderType disp)
     (Obj : I -> lmodType R)
     (bonding : forall i j, i <= j -> {linear Obj j -> Obj i})
     (Sys : is_invsys bonding)
@@ -1006,14 +989,14 @@ HB.end.
 
 HB.factory Record InvLim_isLalgInvLim
     (R : ringType)
-    (disp : unit) (I : porderType disp)
+    disp (I : porderType disp)
     (Obj : I -> lalgType R)
     (bonding : forall i j, i <= j -> {lrmorphism Obj j -> Obj i})
     (Sys : is_invsys bonding)
   ilT of InvLim _ Sys ilT := {}.
 HB.builders Context
     (R : ringType)
-    (disp : unit) (I : porderType disp)
+    disp (I : porderType disp)
     (Obj : I -> lalgType R)
     (bonding : forall i j, i <= j -> {lrmorphism Obj j -> Obj i})
     (Sys : is_invsys bonding)
@@ -1038,14 +1021,14 @@ HB.end.
 
 HB.factory Record InvLim_isAlgebraInvLim
     (R : ringType)
-    (disp : unit) (I : porderType disp)
+    disp (I : porderType disp)
     (Obj : I -> algType R)
     (bonding : forall i j, i <= j -> {lrmorphism Obj j -> Obj i})
     (Sys : is_invsys bonding)
   ilT of InvLim _ Sys ilT := {}.
 HB.builders Context
     (R : ringType)
-    (disp : unit) (I : porderType disp)
+    disp (I : porderType disp)
     (Obj : I -> algType R)
     (bonding : forall i j, i <= j -> {lrmorphism Obj j -> Obj i})
     (Sys : is_invsys bonding)
@@ -1076,7 +1059,7 @@ Close Scope ring_scope.
 (***************************************************************************)
 Section Implem.
 
-Variables (disp : unit) (I : porderType disp).
+Variables (disp : _) (I : porderType disp).
 Variable Obj : I -> Type.
 Variable bonding : forall i j, i <= j -> Obj j -> Obj i.
 Variable Sys : is_invsys bonding.
@@ -1098,7 +1081,7 @@ Notation "{ 'invlim' S }" := (invlim S).
 
 Section InverseLimitTheory.
 
-Variables (disp : unit) (I : porderType disp).
+Variables (disp : _) (I : porderType disp).
 Variable Obj : I -> Type.
 Variable bonding : forall i j, i <= j -> Obj j -> Obj i.
 Variable Sys : is_invsys bonding.
@@ -1155,7 +1138,7 @@ Open Scope ring_scope.
 
 Section Instances.
 
-Variables (disp : unit) (I : porderType disp).
+Variables (disp : _) (I : porderType disp).
 
 Section Nmodule.
 Variable Obj : I -> nmodType.
@@ -1262,6 +1245,7 @@ Variable Sys : is_invsys bonding.
 HB.instance Definition _ := GRing.Algebra.on {invlim Sys}.
 End ComAlg.
 
+(* Just a join 
 Section ComUnitAlg.
 Variables (R : comUnitRingType).
 Variable Obj : I -> comAlgType R.
@@ -1269,11 +1253,12 @@ Variable bonding : forall i j, (i <= j)%O -> {lrmorphism Obj j -> Obj i}.
 Variable Sys : is_invsys bonding.
 HB.instance Definition _ := GRing.Algebra.on {invlim Sys}.
 End ComUnitAlg.
+*)
 
 End Instances.
 
 Section IDomain.
-Variables (disp : unit) (I : dirType disp).
+Variables (disp : _) (I : dirType disp).
 Variable Obj : I -> idomainType.
 Variable bonding : forall i j, i <= j -> {rmorphism Obj j -> Obj i}.
 Variable Sys : is_invsys bonding.
@@ -1283,7 +1268,7 @@ Let test : idomainInvLimType _ := {invlim Sys}.
 End IDomain.
 
 Section Field.
-Variables (disp : unit) (I : dirType disp).
+Variables (disp : _) (I : dirType disp).
 Variable Obj : I -> fieldType.
 Variable bonding : forall i j, i <= j -> {rmorphism Obj j -> Obj i}.
 Variable Sys : is_invsys bonding.
@@ -1295,7 +1280,7 @@ End Field.
 
 Section TestComUnitAlg.
 Variables (R : ringType).
-Variables (disp : unit) (I : porderType disp).
+Variables (disp : _) (I : porderType disp).
 Variable Obj : I -> comUnitAlgType R.
 Variable bonding : forall i j, i <= j -> {lrmorphism Obj j -> Obj i}.
 Variable Sys : is_invsys bonding.
@@ -1561,7 +1546,7 @@ End ValuationUnitRing.
 
 Section CommHugeOp.
 
-Variables (disp : unit) (I : porderType disp).
+Variables (disp : _) (I : porderType disp).
 Variable Obj : I -> choiceType.
 Variable bonding : forall i j : I, i <= j -> Obj j -> Obj i.
 Variable Sys : is_invsys bonding.
@@ -1659,7 +1644,7 @@ End CommHugeOp.
 
 Section Summable.
 
-Variables (disp : unit) (I : porderType disp).
+Variables (disp : _) (I : porderType disp).
 Variable Obj : I -> zmodType.
 Variable bonding : forall i j, i <= j -> {additive Obj j -> Obj i}.
 Variable Sys : is_invsys bonding.
@@ -1719,7 +1704,7 @@ End Summable.
 
 Section Prodable.
 
-Variables (disp : unit) (I : porderType disp).
+Variables (disp : _) (I : porderType disp).
 Variable Obj : I -> comRingType.
 Variable bonding : forall i j, i <= j -> {rmorphism Obj j -> Obj i}.
 Variable Sys : is_invsys bonding.
diff --git a/theories/fps/natbar.v b/theories/fps/natbar.v
index 14236a4..2052a52 100644
--- a/theories/fps/natbar.v
+++ b/theories/fps/natbar.v
@@ -101,7 +101,7 @@ Definition lebar u v :=
   | Nat m, Nat n => m <= n
   | _, _ => false
   end.
-Definition lebar_display : unit. Proof. exact: tt. Qed.
+Definition lebar_display : Order.disp_t. Proof. by []. Qed.
 
 Fact lebar_refl : reflexive lebar.
 Proof. by case=> [m|] /=. Qed.
@@ -128,7 +128,7 @@ Proof. by []. Qed.
 Lemma ltEnatbar (n m : nat) : (Nat n < Nat m) = (n < m)%N.
 Proof. by rewrite lt_neqAle leEnatbar Nat_eqE ltn_neqAle. Qed.
 
-Lemma omorphNat_subproof : Order.order_morphism Nat.
+Lemma omorphNat_subproof : {homo Nat : x y / x <= y}.
 Proof. by move=> x y; rewrite leEnatbar leEnat. Qed.
 HB.instance Definition _ :=
   Order.isOrderMorphism.Build _ _ _ _ Nat omorphNat_subproof.
diff --git a/theories/fps/padic.v b/theories/fps/padic.v
index 9c29511..6da9d5b 100644
--- a/theories/fps/padic.v
+++ b/theories/fps/padic.v
@@ -289,7 +289,7 @@ rewrite -raddfD /=; apply valuatNatE.
   move: pix piy; rewrite {x}eqx {y}eqy mulrACA -exprD !padicp_MpXn_eq0 {vx vy}.
   rewrite rmorphM /=; move: (_ a) (_ b) => {}a {}b.
   (* Fixed bad mathcomp statement *)
-  have Fp_Zcast : Zp_trunc (pdiv p) = Zp_trunc p by have[]:= Fp_Zcast p_pr.
+  have Fp_Zcast : Zp_trunc (pdiv p) = Zp_trunc p by have:= Fp_Zcast p_pr.
   rewrite expn1 -Fp_Zcast in a b |- *.
   exact: mulf_neq0.
 rewrite natrE=> i lti.
@@ -316,6 +316,8 @@ Proof. by rewrite padic_unit valuat_eq0P. Qed.
 
 Fact padic_mul_eq0 x y : x * y = 0 -> (x == 0) || (y == 0).
 Proof. by move/eqP; rewrite -!valuat0P valuatM addbar_eqI. Qed.
+
+HB.instance Definition _ := GRing.ComUnitRing.on (padic_int p_pr).
 HB.instance Definition _ :=
   GRing.ComUnitRing_isIntegral.Build (padic_int p_pr) padic_mul_eq0.
 
diff --git a/theories/fps/tfps.v b/theories/fps/tfps.v
index 9496365..ac07e87 100644
--- a/theories/fps/tfps.v
+++ b/theories/fps/tfps.v
@@ -123,7 +123,7 @@ Reserved Notation "[ 'tfps' s <= n => F ]"
   (at level 0, n at next level, s name, format "[ 'tfps' s <= n  =>  F ]").
 Reserved Notation "[ 'tfps' s => F ]"
   (at level 0, s name, format "[ 'tfps'  s  =>  F ]").
-Reserved Notation "c %:S" (at level 2, format "c %:S").
+Reserved Notation "c %:S" (at level 1, format "c %:S").
 Reserved Notation "\X" (at level 0).
 Reserved Notation "\Xo( n )" (at level 0).
 Reserved Notation "x ^^ n" (at level 29, left associativity).