7 files changed, 71 insertions, 51 deletions
diff --git a/mathcomp/ssreflect/choice.v b/mathcomp/ssreflect/choice.v
index 6f46832..57b585e 100644
--- a/mathcomp/ssreflect/choice.v
+++ b/mathcomp/ssreflect/choice.v
@@ -141,6 +141,9 @@ Proof. by case. Qed.
 
 End OtherEncodings.
 
+Prenex Implicits seq_of_opt tag_of_pair pair_of_tag opair_of_sum sum_of_opair.
+Prenex Implicits seq_of_optK tag_of_pairK pair_of_tagK opair_of_sumK.
+
 (* Generic variable-arity tree type, providing an encoding target for         *)
 (* miscellaneous user datatypes. The GenTree.tree type can be combined with   *)
 (* a sigT type to model multi-sorted concrete datatypes.                      *)
@@ -562,8 +565,8 @@ Export Countable.Exports.
 
 Definition unpickle T := Countable.unpickle (Countable.class T).
 Definition pickle T := Countable.pickle (Countable.class T).
-Arguments unpickle {T}.
-Prenex Implicits pickle.
+Arguments unpickle {T} n.
+Arguments pickle {T} x.
 
 Section CountableTheory.
 
@@ -609,6 +612,11 @@ Notation "[ 'countMixin' 'of' T 'by' <: ]" :=
     (sub_countMixin _ : Countable.mixin_of T)
   (at level 0, format "[ 'countMixin'  'of'  T  'by'  <: ]") : form_scope.
 
+Arguments pickle_inv {T} n.
+Arguments pickleK {T} x.
+Arguments pickleK_inv {T} x.
+Arguments pickle_invK {T} n : rename.
+
 Section SubCountType.
 
 Variables (T : choiceType) (P : pred T).
diff --git a/mathcomp/ssreflect/eqtype.v b/mathcomp/ssreflect/eqtype.v
index dc3daf0..58ef844 100644
--- a/mathcomp/ssreflect/eqtype.v
+++ b/mathcomp/ssreflect/eqtype.v
@@ -514,7 +514,8 @@ Structure subType : Type := SubType {
   _ : forall x Px, val (@Sub x Px) = x
 }.
 
-Arguments Sub [s].
+(* Generic proof that the second property holds by conversion.                *)
+(* The vrefl_rect alias is used to flag generic proofs of the first property. *)
 Lemma vrefl : forall x, P x -> x = x. Proof. by []. Qed.
 Definition vrefl_rect := vrefl.
 
@@ -522,18 +523,21 @@ Definition clone_subType U v :=
   fun sT & sub_sort sT -> U =>
   fun c Urec cK (sT' := @SubType U v c Urec cK) & phant_id sT' sT => sT'.
 
+Section Theory.
+
 Variable sT : subType.
 
+Local Notation val := (@val sT).
+Local Notation Sub x Px := (@Sub sT x Px).
+
 Variant Sub_spec : sT -> Type := SubSpec x Px : Sub_spec (Sub x Px).
 
 Lemma SubP u : Sub_spec u.
-Proof. by case: sT Sub_spec SubSpec u => T' _ C rec /= _. Qed.
+Proof. by case: sT Sub_spec SubSpec u => /= U _ mkU rec _. Qed.
 
-Lemma SubK x Px : @val sT (Sub x Px) = x.
-Proof. by case: sT. Qed.
+Lemma SubK x Px : val (Sub x Px) = x. Proof. by case: sT. Qed.
 
-Definition insub x :=
-  if @idP (P x) is ReflectT Px then @Some sT (Sub x Px) else None.
+Definition insub x := if idP is ReflectT Px then Some (Sub x Px) else None.
 
 Definition insubd u0 x := odflt u0 (insub x).
 
@@ -561,49 +565,55 @@ Proof. by move/negPf/insubF. Qed.
 Lemma isSome_insub : ([eta insub] : pred T) =1 P.
 Proof. by apply: fsym => x; case: insubP => // /negPf. Qed.
 
-Lemma insubK : ocancel insub (@val _).
+Lemma insubK : ocancel insub val.
 Proof. by move=> x; case: insubP. Qed.
 
-Lemma valP (u : sT) : P (val u).
+Lemma valP u : P (val u).
 Proof. by case/SubP: u => x Px; rewrite SubK. Qed.
 
-Lemma valK : pcancel (@val _) insub.
+Lemma valK : pcancel val insub.
 Proof. by case/SubP=> x Px; rewrite SubK; apply: insubT. Qed.
 
-Lemma val_inj : injective (@val sT).
+Lemma val_inj : injective val.
 Proof. exact: pcan_inj valK. Qed.
 
-Lemma valKd u0 : cancel (@val _) (insubd u0).
+Lemma valKd u0 : cancel val (insubd u0).
 Proof. by move=> u; rewrite /insubd valK. Qed.
 
 Lemma val_insubd u0 x : val (insubd u0 x) = if P x then x else val u0.
 Proof. by rewrite /insubd; case: insubP => [u -> | /negPf->]. Qed.
 
-Lemma insubdK u0 : {in P, cancel (insubd u0) (@val _)}.
+Lemma insubdK u0 : {in P, cancel (insubd u0) val}.
 Proof. by move=> x Px; rewrite /= val_insubd [P x]Px. Qed.
 
-Definition insub_eq x :=
-  let Some_sub Px := Some (Sub x Px : sT) in
-  let None_sub _ := None in
-  (if P x as Px return P x = Px -> _ then Some_sub else None_sub) (erefl _).
+Let insub_eq_aux x isPx : P x = isPx -> option sT :=
+  if isPx as b return _ = b -> _ then fun Px => Some (Sub x Px) else fun=> None.
+Definition insub_eq x := insub_eq_aux (erefl (P x)).
 
 Lemma insub_eqE : insub_eq =1 insub.
 Proof.
-rewrite /insub_eq /insub => x; case: {2 3}_ / idP (erefl _) => // Px Px'.
-by congr (Some _); apply: val_inj; rewrite !SubK.
+rewrite /insub_eq => x; set b := P x; rewrite [in LHS]/b in (Db := erefl b) *.
+by case: b in Db *; [rewrite insubT | rewrite insubF].
 Qed.
 
+End Theory.
+
 End SubType.
 
-Arguments SubType [T P].
-Arguments Sub {T P s}.
-Arguments vrefl {T P}.
-Arguments vrefl_rect {T P}.
+Arguments SubType {T P} sub_sort val Sub rec SubK.
+Arguments val {T P sT} u : rename.
+Arguments Sub {T P sT} x Px : rename.
+Arguments vrefl {T P} x Px.
+Arguments vrefl_rect {T P} x Px.
 Arguments clone_subType [T P] U v [sT] _ [c Urec cK].
-Arguments insub {T P sT}.
+Arguments insub {T P sT} x.
+Arguments insubd {T P sT} u0 x.
 Arguments insubT [T] P [sT x].
-Arguments val_inj {T P sT} [x1 x2].
-Prenex Implicits val insubd.
+Arguments val_inj {T P sT} [u1 u2] eq_u12 : rename.
+Arguments valK {T P sT} u : rename.
+Arguments valKd {T P sT} u0 u : rename.
+Arguments insubK {T P} sT x.
+Arguments insubdK {T P sT} u0 [x] Px.
 
 Local Notation inlined_sub_rect :=
   (fun K K_S u => let (x, Px) as u return K u := u in K_S x Px).
@@ -623,10 +633,6 @@ Notation "[ 'subType' 'for' v 'by' rec ]" := (SubType _ v _ rec vrefl)
 Notation "[ 'subType' 'of' U 'for' v ]" := (clone_subType U v id idfun)
  (at level 0, format "[ 'subType'  'of'  U  'for'  v ]") : form_scope.
 
-(*
-Notation "[ 'subType' 'for' v ]" := (clone_subType _ v id idfun)
- (at level 0, format "[ 'subType'  'for'  v ]") : form_scope.
-*)
 Notation "[ 'subType' 'of' U ]" := (clone_subType U _ id id)
  (at level 0, format "[ 'subType'  'of'  U ]") : form_scope.
 
diff --git a/mathcomp/ssreflect/finfun.v b/mathcomp/ssreflect/finfun.v
index 9929e82..db1a8e7 100644
--- a/mathcomp/ssreflect/finfun.v
+++ b/mathcomp/ssreflect/finfun.v
@@ -147,6 +147,7 @@ End PlainTheory.
 Notation family F := (family_mem (fun_of_simpl (fmem F))).
 Notation ffun_on R := (ffun_on_mem _ (mem R)).
 
+Arguments ffunK {aT rT}.
 Arguments familyP {aT rT pT F f}.
 Arguments ffun_onP {aT rT R f}.
 
diff --git a/mathcomp/ssreflect/finset.v b/mathcomp/ssreflect/finset.v
index 9ca96c8..87d5da4 100644
--- a/mathcomp/ssreflect/finset.v
+++ b/mathcomp/ssreflect/finset.v
@@ -2206,6 +2206,7 @@ Qed.
 
 End MaxSetMinSet.
 
+Arguments setCK {T}.
 Arguments minsetP {T P A}.
 Arguments maxsetP {T P A}.
 Prenex Implicits minset maxset.
diff --git a/mathcomp/ssreflect/fintype.v b/mathcomp/ssreflect/fintype.v
index 441fc12..06aca24 100644
--- a/mathcomp/ssreflect/fintype.v
+++ b/mathcomp/ssreflect/fintype.v
@@ -1485,7 +1485,7 @@ Proof. by rewrite mem_undup mem_pmap -valK map_f ?ssvalP. Qed.
 Lemma val_seq_sub_enum : uniq s -> map val seq_sub_enum = s.
 Proof.
 move=> Us; rewrite /seq_sub_enum undup_id ?pmap_sub_uniq //.
-rewrite (pmap_filter (@insubK _ _ _)); apply/all_filterP.
+rewrite (pmap_filter (insubK _)); apply/all_filterP.
 by apply/allP => x; rewrite isSome_insub.
 Qed.
 
@@ -1646,13 +1646,13 @@ Lemma rev_ord_proof n (i : 'I_n) : n - i.+1  < n.
 Proof. by case: n i => [|n] [i lt_i_n] //; rewrite ltnS subSS leq_subr. Qed.
 Definition rev_ord n i := Ordinal (@rev_ord_proof n i).
 
-Lemma rev_ordK n : involutive (@rev_ord n).
+Lemma rev_ordK {n} : involutive (@rev_ord n).
 Proof.
 by case: n => [|n] [i lti] //; apply: val_inj; rewrite /= !subSS subKn.
 Qed.
 
 Lemma rev_ord_inj {n} : injective (@rev_ord n).
-Proof. exact: inv_inj (@rev_ordK n). Qed.
+Proof. exact: inv_inj rev_ordK. Qed.
 
 (* bijection between any finType T and the Ordinal finType of its cardinal *)
 Section EnumRank.
@@ -1762,7 +1762,7 @@ End EnumRank.
 
 Arguments enum_val_inj {T A} [i1 i2] : rename.
 Arguments enum_rank_inj {T} [x1 x2].
-Prenex Implicits enum_val enum_rank.
+Prenex Implicits enum_val enum_rank enum_valK enum_rankK.
 
 Lemma enum_rank_ord n i : enum_rank i = cast_ord (esym (card_ord n)) i.
 Proof.
@@ -1800,8 +1800,8 @@ case: (ltngtP i h) => /= [-> | ltih | ->] //; last by rewrite ltnn.
 by rewrite subn1 /= leqNgt !(ltn_predK ltih, ltih, add1n).
 Qed.
 
-Lemma unbumpK h : {in predC1 h, cancel (unbump h) (bump h)}.
-Proof. by move=> i; move/negbTE=> neq_h_i; rewrite unbumpKcond neq_h_i. Qed.
+Lemma unbumpK {h} : {in predC1 h, cancel (unbump h) (bump h)}.
+Proof. by move=> i /negbTE-neq_h_i; rewrite unbumpKcond neq_h_i. Qed.
 
 Lemma bump_addl h i k : bump (k + h) (k + i) = k + bump h i.
 Proof. by rewrite /bump leq_add2l addnCA. Qed.
@@ -1882,15 +1882,11 @@ by case Dui: (unlift h i) / (unliftP h i) => [j Dh|//]; exists j.
 Qed.
 
 Lemma lift_inj n (h : 'I_n) : injective (lift h).
-Proof.
-move=> i1 i2; move/eqP; rewrite [_ == _](can_eq (@bumpK _)) => eq_i12.
-exact/eqP.
-Qed.
+Proof. by move=> i1 i2 [/(can_inj (bumpK h))/val_inj]. Qed.
+Arguments lift_inj {n h} [i1 i2] eq_i12h : rename.
 
 Lemma liftK n (h : 'I_n) : pcancel (lift h) (unlift h).
-Proof.
-by move=> i; case: (unlift_some (neq_lift h i)) => j; move/lift_inj->.
-Qed.
+Proof. by move=> i; case: (unlift_some (neq_lift h i)) => j /lift_inj->. Qed.
 
 (* Shifting and splitting indices, for cutting and pasting arrays *)
 
@@ -1906,7 +1902,7 @@ Definition rshift m n (i : 'I_n) := Ordinal (rshift_subproof m i).
 Lemma split_subproof m n (i : 'I_(m + n)) : i >= m -> i - m < n.
 Proof. by move/subSn <-; rewrite leq_subLR. Qed.
 
-Definition split m n (i : 'I_(m + n)) : 'I_m + 'I_n :=
+Definition split {m n} (i : 'I_(m + n)) : 'I_m + 'I_n :=
   match ltnP (i) m with
   | LtnNotGeq lt_i_m =>  inl _ (Ordinal lt_i_m)
   | GeqNotLtn ge_i_m =>  inr _ (Ordinal (split_subproof ge_i_m))
@@ -1922,16 +1918,16 @@ rewrite /split {-3}/leq.
 by case: (@ltnP i m) => cmp_i_m //=; constructor; rewrite ?subnKC.
 Qed.
 
-Definition unsplit m n (jk : 'I_m + 'I_n) :=
+Definition unsplit {m n} (jk : 'I_m + 'I_n) :=
   match jk with inl j => lshift n j | inr k => rshift m k end.
 
 Lemma ltn_unsplit m n (jk : 'I_m + 'I_n) : (unsplit jk < m) = jk.
 Proof. by case: jk => [j|k]; rewrite /= ?ltn_ord // ltnNge leq_addr. Qed.
 
-Lemma splitK m n : cancel (@split m n) (@unsplit m n).
+Lemma splitK {m n} : cancel (@split m n) unsplit.
 Proof. by move=> i; apply: val_inj; case: splitP. Qed.
 
-Lemma unsplitK m n : cancel (@unsplit m n) (@split m n).
+Lemma unsplitK {m n} : cancel (@unsplit m n) split.
 Proof.
 move=> jk; have:= ltn_unsplit jk.
 by do [case: splitP; case: jk => //= i j] => [|/addnI] => /ord_inj->.
@@ -1979,6 +1975,8 @@ Arguments ord0 {n'}.
 Arguments ord_max {n'}.
 Arguments inord {n'}.
 Arguments sub_ord {n'}.
+Arguments sub_ordK {n'}.
+Arguments inord_val {n'}.
 
 (* Product of two fintypes which is a fintype *)
 Section ProdFinType.
diff --git a/mathcomp/ssreflect/generic_quotient.v b/mathcomp/ssreflect/generic_quotient.v
index b7a8444..71fd10a 100644
--- a/mathcomp/ssreflect/generic_quotient.v
+++ b/mathcomp/ssreflect/generic_quotient.v
@@ -144,6 +144,8 @@ Definition QuotType_clone (Q : Type) qT cT
 
 End QuotientDef.
 
+Arguments repr_ofK {T qT}.
+
 (****************************)
 (* Protecting some symbols. *)
 (****************************)
@@ -195,7 +197,7 @@ Notation QuotType Q m := (@QuotTypePack _ Q m).
 Notation "[ 'quotType' 'of' Q ]" := (@QuotType_clone _ Q _ _ id)
  (at level 0, format "[ 'quotType'  'of'  Q ]") : form_scope.
 
-Arguments repr {T qT}.
+Arguments repr {T qT} x.
 
 (************************)
 (* Exporting the theory *)
@@ -227,6 +229,8 @@ Proof. by move=> Py x; rewrite -[x]reprK; apply: Py; rewrite reprK. Qed.
 
 End QuotTypeTheory.
 
+Arguments reprK {T qT} x.
+
 (*******************)
 (* About morphisms *)
 (*******************)
@@ -657,6 +661,8 @@ Canonical EquivQuot.eqType.
 Canonical EquivQuot.choiceType.
 Canonical EquivQuot.eqQuotType.
 
+Arguments EquivQuot.ereprK {D C CD DC eD encD}.
+
 Notation "{eq_quot e }" :=
 (@EquivQuot.type_of _ _ _ _ _ _ (Phantom (rel _) e)) : quotient_scope.
 Notation "x == y %[mod_eq r ]" := (x == y %[mod {eq_quot r}]) : quotient_scope.
@@ -690,7 +696,7 @@ Variables (eD : equiv_rel D) (encD : encModRel CD DC eD).
 Notation eC := (encoded_equiv encD).
 
 Fact eq_quot_countMixin : Countable.mixin_of {eq_quot encD}.
-Proof. exact: CanCountMixin (@EquivQuot.ereprK _ _ _ _ _ _). Qed.
+Proof. exact: CanCountMixin EquivQuot.ereprK. Qed.
 Canonical eq_quot_countType := CountType {eq_quot encD} eq_quot_countMixin.
 
 End CountEncodingModuloRel.
diff --git a/mathcomp/ssreflect/tuple.v b/mathcomp/ssreflect/tuple.v
index 9154eb5..8f81155 100644
--- a/mathcomp/ssreflect/tuple.v
+++ b/mathcomp/ssreflect/tuple.v
@@ -336,7 +336,7 @@ Definition enum : seq (n.-tuple T) :=
 
 Lemma enumP : Finite.axiom enum.
 Proof.
-case=> /= t t_n; rewrite -(count_map _ (pred1 t)) (pmap_filter (@insubK _ _ _)).
+case=> /= t t_n; rewrite -(count_map _ (pred1 t)) (pmap_filter (insubK _)).
 rewrite count_filter -(@eq_count _ (pred1 t)) => [|s /=]; last first.
   by rewrite isSome_insub; case: eqP=> // ->.
 elim: n t t_n => [|m IHm] [|x t] //= {IHm}/IHm; move: (iter m _ _) => em IHm.