Fix a few warnings

src/bool.v

@@ -925,23 +925,21 @@ Proof. by case b1; case b2; constructor; auto. Qed.
 
 End ReflectConnectives.
 
-Arguments idP [b1].
-Arguments idPn [b1].
-Arguments negP [b1].
-Arguments negPn [b1].
-Arguments negPf [b1].
-Arguments andP [b1 b2].
-Arguments and3P [b1 b2 b3].
-Arguments and4P [b1 b2 b3 b4].
-Arguments and5P [b1 b2 b3 b4 b5].
-Arguments orP [b1 b2].
-Arguments or3P [b1 b2 b3].
-Arguments or4P [b1 b2 b3 b4].
-Arguments nandP [b1 b2].
-Arguments norP [b1 b2].
-Arguments implyP [b1 b2].
-Prenex Implicits idP idPn negP negPn negPf.
-Prenex Implicits andP and3P and4P and5P orP or3P or4P nandP norP implyP.
+Arguments idP {b1}.
+Arguments idPn {b1}.
+Arguments negP {b1}.
+Arguments negPn {b1}.
+Arguments negPf {b1}.
+Arguments andP {b1 b2}.
+Arguments and3P {b1 b2 b3}.
+Arguments and4P {b1 b2 b3 b4}.
+Arguments and5P {b1 b2 b3 b4 b5}.
+Arguments orP {b1 b2}.
+Arguments or3P {b1 b2 b3}.
+Arguments or4P {b1 b2 b3 b4}.
+Arguments nandP {b1 b2}.
+Arguments norP {b1 b2}.
+Arguments implyP {b1 b2}.
 
 (**  Shorter, more systematic names for the boolean connectives laws.        **)
 
@@ -1065,7 +1063,7 @@ Proof. by case: a; case: b. Qed.
 
 Lemma addbP a b : reflect (~~ a = b) (a (+) b).
 Proof. by case: a; case: b; constructor. Qed.
-Arguments addbP [a b].
+Arguments addbP {a b}.
 
 (**
  Resolution tactic for blindly weeding out common terms from boolean
@@ -1252,7 +1250,7 @@ Unset Primitive Projections.
 Structure predType := PredType {
   pred_sort :> Type;
   topred : pred_sort -> pred T;
-  _predType_2: {mem | isMem topred mem}
+  _: {mem | isMem topred mem}
 }.
 Set Primitive Projections.
 
@@ -1271,9 +1269,9 @@ Definition clone_pred U :=
 
 End Predicates.
 
-Arguments pred0 [T].
-Arguments predT [T].
-Prenex Implicits pred0 predT predI predU predC predD preim relU.
+Arguments pred0 {T}.
+Arguments predT {T}.
+Prenex Implicits predI predU predC predD preim relU.
 
 Notation "[ 'pred' : T | E ]" := (SimplPred (fun _ : T => E%B))
   (at level 0, format "[ 'pred' :  T  |  E ]") : fun_scope.

src/eqtype.v

@@ -58,7 +58,7 @@ Import functions.
 (* Equality on an eqType is proof-irrelevant (lemma eq_irrelevance).          *)
 (*   The eqType interface is implemented for most standard datatypes:         *)
 (*  bool, unit, void, option, prod (denoted A * B), sum (denoted A + B),      *)
-(*  sig (denoted {x | P}), sigT (denoted {i : I & T}). We also define         *)
+(*  sig (denoted {x | P}). We also define         *)
 (*   tagged_as u v == v cast as T_(tag u) if tag v == tag u, else u.          *)
 (*  -> We have u == v <=> (tag u == tag v) && (tagged u == tagged_as u v).    *)
 (* The subType interface supports the following operations:                   *)
@@ -165,6 +165,7 @@ Lemma eqP T : Equality.axiom (@eq_op T).
 Proof. by case: T => ? []. Qed.
 Arguments eqP {T x y}.
 
+Declare Scope eq_scope.
 Delimit Scope eq_scope with EQ.
 Open Scope eq_scope.
 
@@ -462,6 +463,8 @@ End FunWith.
 
 Prenex Implicits fwith.
 
+Declare Scope fun_delta_scope.
+
 Notation "x |-> y" := (FunDelta x y)
   (at level 190, no associativity,
    format "'[hv' x '/ '  |->  y ']'") : fun_delta_scope.
@@ -809,7 +812,7 @@ Arguments opt_eq {T} !u !v.
 Section TaggedAs.
 
 Variables (I : eqType) (T_ : I -> Type).
-Implicit Types u v : {i : I | T_ i}.
+Implicit Types u v : { i : I | T_ i }.
 
 Definition tagged_as u v :=
   if tag u =P tag v is ReflectT eq_uv then
@@ -826,7 +829,7 @@ End TaggedAs.
 Section TagEqType.
 
 Variables (I : eqType) (T_ : I -> eqType).
-Implicit Types u v : {i : I | T_ i}.
+Implicit Types u v : Tag T_.
 
 Definition tag_eq u v := (tag u == tag v) && (tagged u == tagged_as u v).
 
@@ -838,20 +841,14 @@ by apply: (iffP eqP) => [->|<-]; rewrite tagged_asE.
 Qed.
 
 Canonical tag_eqMixin := EqMixin tag_eqP.
-Canonical tag_eqType := Eval hnf in EqType {i : I | T_ i} tag_eqMixin.
+Canonical tag_eqType := Eval hnf in EqType (Tag T_) tag_eqMixin.
 
-(* FIXME: the “tag_eqType” should be inferred *)
-Fail Lemma tag_eqE : tag_eq = eq_op.
-Lemma tag_eqE : tag_eq = @eq_op (tag_eqType). Proof. by []. Qed.
+Lemma tag_eqE : tag_eq = eq_op. Proof. by []. Qed.
 
-(* FIXME: the “tag_eqType” should be inferred *)
-Fail Lemma eq_tag u v : u == v -> tag u = tag v.
-Lemma eq_tag (u v: tag_eqType) : u == v -> tag u = tag v.
+Lemma eq_tag u v : u == v -> tag u = tag v.
 Proof. by move/eqP->. Qed.
 
-(* FIXME: the “tag_eqType” should be inferred *)
-Fail Lemma eq_Tagged u x : (u == Tagged _ x) = (tagged u == x).
-Lemma eq_Tagged (u: tag_eqType) x : (u == Tagged _ x) = (tagged u == x).
+Lemma eq_Tagged u x : (u == Tagged _ x) = (tagged u == x).
 Proof. by rewrite -tag_eqE /tag_eq eqxx tagged_asE. Qed.
 
 End TagEqType.

src/functions.v

@@ -401,6 +401,7 @@ Section Tag.
 
 Variables (I : Type) (i : I) (T_ U_ : I -> Type).
 
+Definition Tag := sig T_.
 Definition tag := sig_proj1.
 Definition tagged : forall w, T_(tag w) := @sig_proj2 I [eta T_].
 Definition Tagged x := @exist I [eta T_] i x.