Merge pull request #142 from math-comp/mathcomp-1.9.0

compat with mathcomp 1.9.0

classical_sets.v

@@ -163,7 +163,7 @@ Canonical Prop_choiceType := ChoiceType Prop gen_choiceMixin.
 
 Definition set A := A -> Prop.
 Definition in_set T (P : set T) : pred T := [pred x | `[<P x>]].
-Canonical set_predType T := @mkPredType T (set T) (@in_set T).
+Canonical set_predType T := @PredType T (set T) (@in_set T).
 
 Lemma in_setE T (P : set T) x : x \in P = P x :> Prop.
 Proof. by rewrite propeqE; split => [] /asboolP. Qed.

derive.v

@@ -397,7 +397,7 @@ suff /diff_locally /hdf -> : differentiable f x.
 apply/diffP; apply: (@getPex _ (fun (df : {linear V -> W}) => continuous df /\
   forall y, f y = f (lim x) + df (y - lim x) +o_(y \near x) (y - lim x))).
 exists df; split=> //; apply: eqaddoEx => z.
-rewrite (hdf _ dxf) !addrA lim_id /funcomp /= subrK [f _ + _]addrC addrK.
+rewrite (hdf _ dxf) !addrA lim_id /(_ \o _) /= subrK [f _ + _]addrC addrK.
 rewrite -addrA -[LHS]addr0; congr (_ + _).
 apply/eqP; rewrite eq_sym addrC addr_eq0 oppox; apply/eqP.
 by rewrite littleo_center0 (comp_centerK x id) -[- _ in RHS](comp_centerK x).
@@ -1345,7 +1345,7 @@ Proof.
 move=> cvfx; apply/Logic.eq_sym.
 (* should be inferred *)
 have atrF := at_right_proper_filter x.
-apply: flim_map_lim => A /cvfx /locallyP [_ /posnumP[e] xe_A].
+apply: (@flim_map_lim _ _ _ (at_right _)) => A /cvfx /locallyP [_ /posnumP[e] xe_A].
 by exists e%:num => // y xe_y; rewrite ltr_def => /andP [xney _]; apply: xe_A.
 Qed.
 
@@ -1355,7 +1355,7 @@ Proof.
 move=> cvfx; apply/Logic.eq_sym.
 (* should be inferred *)
 have atrF := at_left_proper_filter x.
-apply: flim_map_lim => A /cvfx /locallyP [_ /posnumP[e] xe_A].
+apply: (@flim_map_lim _ _ _ (at_left _)) => A /cvfx /locallyP [_ /posnumP[e] xe_A].
 exists e%:num => // y xe_y; rewrite ltr_def => /andP [xney _].
 by apply: xe_A => //; rewrite eq_sym.
 Qed.

normedtype.v

@@ -795,7 +795,7 @@ Proof. by symmetry; apply: locally_flim_unique; apply/cvg_ex; exists x. Qed.
 
 Lemma flim_lim {F} {FF : ProperFilter F} (l : V) :
   F --> l -> lim F = l.
-Proof. by move=> Fl; have Fcv := cvgP Fl; apply: flim_unique. Qed.
+Proof. by move=> Fl; have Fcv := cvgP Fl; apply: (@flim_unique F). Qed.
 
 Lemma flim_map_lim {T : Type} {F} {FF : ProperFilter F} (f : T -> V) (l : V) :
   f @ F --> l -> lim (f @ F) = l.

topology.v

@@ -804,12 +804,12 @@ Proof. by move=> ????? PQR FP; apply: filter_app2; apply: filter_app FP. Qed.
 Lemma filterS2 (T : Type) (F : set (set T)) :
   Filter F -> forall P Q R : set T, (forall x, P x -> Q x -> R x) ->
   F P -> F Q -> F R.
-Proof. by move=> ???? /filterE; apply: filter_app2. Qed.
+Proof. by move=> ? ? ? ? ?; apply: filter_app2; apply: filterE. Qed.
 
 Lemma filterS3 (T : Type) (F : set (set T)) :
   Filter F -> forall P Q R S : set T, (forall x, P x -> Q x -> R x -> S x) ->
   F P -> F Q -> F R -> F S.
-Proof. by move=> ????? /filterE; apply: filter_app3. Qed.
+Proof. by move=> ? ? ? ? ? ?; apply: filter_app3; apply: filterE. Qed.
 
 Lemma filter_const {T : Type} {F} {FF: @ProperFilter T F} (P : Prop) :
   F (fun=> P) -> P.
@@ -1948,7 +1948,7 @@ Lemma cluster_flimE F :
 Proof.
 move=> FF; rewrite predeqE => p.
 split=> [clFp|[G Gproper [cvGp sFG]] A B]; last first.
-  by move=> /sFG GA /cvGp GB; apply/filter_ex; apply: filterI.
+  by move=> /sFG GA /cvGp GB; apply: (@filter_ex _ G); apply: filterI.
 exists (filter_from (\bigcup_(A in F) [set A `&` B | B in locally p]) id).
   apply filter_from_proper; last first.
     by move=> _ [A FA [B p_B <-]]; have := clFp _ _ FA p_B.
@@ -2009,7 +2009,7 @@ have GF : ProperFilter G.
     move=> C1 C2 F1 F2; exists (C1 `&` C2); first exact: filterI.
     by move=> ?[?[]]; split; split.
   by move=> C /(filterI FfA) /filter_ex [_ [[p ? <-]]]; eexists p.
-case: Aco; first by exists (f @` A) => // ? [].
+case: (Aco G); first by exists (f @` A) => // ? [].
 move=> p [Ap clsGp]; exists (f p); split; first exact/imageP.
 move=> B C FB /fcont; rewrite in_setE /= locally_filterE => /(_ Ap) p_Cf.
 have : G (A `&` f @^-1` B) by exists B.
@@ -2055,7 +2055,7 @@ suff UAF : ProperFilter (\bigcup_(H in A) projT1 H).
   exists (existT _ (\bigcup_(H in A) projT1 H) (conj UAF sFUA)) => H AH B HB /=.
   by exists H.
 apply Build_ProperFilter.
-  by move=> B [H AH HB]; have [HF _] := projT2 H; apply: filter_ex.
+  by move=> B [H AH HB]; have [HF _] := projT2 H; apply: (@filter_ex _ _ HF).
 split; first by exists G => //; apply: filterT.
   move=> B C [HB AHB HBB] [HC AHC HCC]; have [sHBC|sHCB] := Atot _ _ AHB AHC.
     exists HC => //; have [HCF _] := projT2 HC; apply: filterI HCC.
@@ -2199,7 +2199,7 @@ Lemma filter_finI (T : pointedType) (F : set (set T)) (D : set (set T))
   (f : set T -> set T) :
   ProperFilter F -> (forall A, D A -> F (f A)) -> finI D f.
 Proof.
-move=> FF sDFf D' sD; apply/filter_ex; apply: filter_bigI.
+move=> FF sDFf D' sD; apply: (@filter_ex _ F); apply: filter_bigI.
 by move=> A /sD; rewrite in_setE => /sDFf.
 Qed.
 
@@ -2253,8 +2253,8 @@ rewrite predeqE => A; split=> [Aco I D f [g gcl feAg] finIf|Aco F FF FA].
   exists p => j Dj; rewrite feAg //; split=> //; apply: gcl => // B.
   by apply: clfinIfp; exists (f j); [apply: finI_from1|rewrite feAg // => ? []].
 have finIAclF : finI F (fun B => A `&` closure B).
-  apply: filter_finI => B FB; apply: filterI => //; apply: filterS FB.
-  exact: subset_closure.
+  apply: (@filter_finI _ F) => B FB.
+  by apply: filterI => //; apply: filterS FB; apply: subset_closure.
 have [|p AclFIp] := Aco _ _ _ _ finIAclF.
   by exists closure=> //; move=> ??; apply: closed_closure.
 exists p; split=> [|B C FB p_C]; first by have /AclFIp [] := FA.
@@ -2608,7 +2608,7 @@ Lemma flim_closeP (F : set (set M)) (l : M) : ProperFilter F ->
   F --> l <-> ([cvg F in M] /\ close (lim F) l).
 Proof.
 move=> FF; split=> [Fl|[cvF]Cl].
-  by have /cvgP := Fl; split=> //; apply: flim_close.
+  by have /cvgP := Fl; split=> //; apply: (@flim_close F).
 by apply: flim_trans (close_limxx Cl).
 Qed.