Compiles

Author: proux01

_CoqProject

@@ -30,7 +30,6 @@ reals/constructive_ereal.v
 reals/reals.v
 reals/real_interval.v
 reals/signed.v
-reals/interval_inference.v
 reals/prodnormedzmodule.v
 reals/all_reals.v
 experimental_reals/xfinmap.v

analysis_stdlib/showcase/uniform_bigO.v

@@ -53,7 +53,7 @@ wlog lex12 : x / (`|x.1| <= `|x.2|).
   by rewrite addrC [`|_|]maxC (ler_norm (x.2, x.1)).
 rewrite [`|_|]max_r // -[X in X * _]ger0_norm // -normrM.
 rewrite -sqrtr_sqr ler_wsqrtr // exprMn sqr_sqrtr // mulr_natl mulr2n lerD2r.
-rewrite -[_ ^+ 2]ger0_norm ?sqr_ge0 // -[X in _ <=X]ger0_norm ?sqr_ge0 //.
+rewrite -[leLHS]ger0_norm ?sqr_ge0 // -[leRHS]ger0_norm ?sqr_ge0 //.
 by rewrite !normrX lerXn2r // nnegrE normr_ge0.
 Qed.
 

classical/cardinality.v

@@ -560,8 +560,13 @@ split=> [Ainfinite| + /finite_setP[n eqAI]]; last first.
 have /all_sig2[f Af fX] : forall X : {fset T}, {x | x \in A & x \notin X}.
   move=> X; apply/sig2W; apply: contra_notP Ainfinite => nAX; apply/finite_fsetP.
   exists [fset x in X | x \in A]%fset; rewrite eqEsubset; split; last first.
-    by move=> x/=; rewrite !inE => /andP[_]; rewrite inE.
-  move=> x Ax /=; rewrite !inE/=; apply/andP; split; rewrite ?inE//.
+    (* move=> x/=. *)
+(* Set SsrMatching LegacyFoUnif. *)  (* TODO: investigate *)
+(* rewrite [in X in X -> _]mem_filterf. *)
+    by move=> x/=; rewrite in_fset inE => /andP[_]; rewrite inE.
+  (* by move=> x/=; rewrite !inE => /andP[_]; rewrite inE. *)
+  move=> x Ax /=; rewrite in_fset inE/=; apply/andP; split; rewrite ?inE//.  (* TODO: same *)
+  (* move=> x Ax /=; rewrite !inE/=; apply/andP; split; rewrite ?inE//. *)
   by apply: contra_notT nAX => xNX; exists x; rewrite ?inE.
 do [under [forall x : {fset _}, _]eq_forall do rewrite inE] in Af *.
 suff [g gE] : exists g : nat -> T,

classical/functions.v

@@ -2456,7 +2456,7 @@ End set_bij_lemmas.
 Lemma bij_II_D1 T n (A : set T) (f : nat -> T) :
   set_bij `I_n.+1 A f -> set_bij `I_n (A `\ f n) f.
 Proof.
-rewrite IIS -image_set1; apply: bij_sub_setUll.
+rewrite IIS -[[set f n]]image_set1; apply: bij_sub_setUll.
 by apply/disj_setPS => i [/= /[swap]->]; rewrite ltnn.
 Qed.
 

reals/all_reals.v

@@ -1,4 +1,3 @@
-From mathcomp Require Export interval_inference.
 From mathcomp Require Export constructive_ereal.
 From mathcomp Require Export reals.
 From mathcomp Require Export real_interval.

reals/constructive_ereal.v

@@ -820,7 +820,7 @@ Proof. exact: raddfMn. Qed.
 
 Lemma prodEFin T s (P : pred T) (f : T -> R) :
   \prod_(i <- s | P i) (f i)%:E = (\prod_(i <- s | P i) f i)%:E.
-Proof. by elim/big_ind2 : _ => // _ x _ y -> ->; rewrite EFinM. Qed.
+Proof. by elim/big_ind2 : _ => // ? x ? y -> ->; rewrite EFinM. Qed.
 
 Lemma sumEFin I s P (F : I -> R) :
   \sum_(i <- s | P i) (F i)%:E = (\sum_(i <- s | P i) F i)%:E.
@@ -916,7 +916,7 @@ Lemma adde_defNN x y : - x +? - y = x +? y.
 Proof. by rewrite adde_defN oppeK. Qed.
 
 Lemma oppe_eq0 x : (- x == 0)%E = (x == 0)%E.
-Proof. by rewrite -(can_eq oppeK) oppe0. Qed.
+Proof. by rewrite -[RHS](can_eq oppeK) oppe0. Qed.
 
 Lemma oppeD x y : x +? y -> - (x + y) = - x - y.
 Proof. by move: x y => [x| |] [y| |] //= _; rewrite opprD. Qed.
@@ -2467,7 +2467,7 @@ move: x => [x|_|//].
   move=> [y| |] [z| |]//; first by rewrite !lee_fin// ler_pM2r.
   - by move=> _; rewrite mulr_infty gtr0_sg// mul1e leey.
   - by move=> _; rewrite mulr_infty gtr0_sg// mul1e leNye.
-  - by move=> _; rewrite 2!mulr_infty gtr0_sg// 2!mul1e.
+  - by move=> _; rewrite mulNyr mulyr gtr0_sg// 2!mul1e.
 move=> [y| |] [z| |]//.
 - rewrite lee_fin => yz.
   have [z0|z0|] := ltgtP 0%R z.