Updating files + reorganizing everything

9 files changed, 71 insertions, 55 deletions

diff --git a/mathcomp/attic/algnum_basic.v b/mathcomp/attic/algnum_basic.v
index a302e7a..53f9016 100644
--- a/mathcomp/attic/algnum_basic.v
+++ b/mathcomp/attic/algnum_basic.v
@@ -1,7 +1,12 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
-Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype tuple div.
+Require Import mathcomp.ssreflect.ssreflect.
+From mathcomp
+Require Import ssrfun ssrbool eqtype ssrnat seq choice fintype tuple div.
+From mathcomp
 Require Import bigop prime finset fingroup ssralg finalg zmodp abelian.
+From mathcomp
 Require Import matrix vector falgebra finfield action poly ssrint cyclotomic.
+From mathcomp
 Require Import fieldext mxalgebra mxpoly.
 
 (************************************************************************************************)
@@ -120,7 +125,7 @@ Qed.
 Lemma int_clos_incl a : a \in A -> integral a.
 Proof.
 move=> ainA; exists ('X - a%:P); rewrite monicXsubC root_XsubC.
-rewrite polyOverXsubC => //; by exact Asubr.
+rewrite polyOverXsubC => //; by apply Asubr.
 Qed.
 
 Lemma intPl (I : eqType) G (r : seq I) l : has (fun x => G x != 0) r ->
@@ -156,7 +161,7 @@ have rs : size r = n.-1 by rewrite /r size_takel // size_opp leq_pred.
 exists r; split.
   apply/eqP => /nilP; rewrite /nilp /r size_takel; last by rewrite size_opp leq_pred.
   by rewrite -subn1 subn_eq0 leqNgt ps.
-  have : - p \is a polyOver A by rewrite rpredN //; exact Asubr.
+  have : - p \is a polyOver A by rewrite rpredN //; apply Asubr.
   by move => /allP-popA; apply/allP => x /mem_take /popA.
 move: pr => /rootP; rewrite horner_coef -(prednK (n := size p)); last by rewrite ltnW.
 rewrite big_ord_recr /= rs; have := monicP pm; rewrite /lead_coef => ->; rewrite mul1r => /eqP.
@@ -283,9 +288,9 @@ pose Y := map_tuple finv Xdual; exists Y => Und Xb.
 have Ydef (i : 'I_m) : Y`_i = finv Xdual`_i by rewrite -!tnth_nth tnth_map.
 have XiU (i : 'I_m) : X`_i \in U by apply/(basis_mem Xb)/mem_nth; rewrite size_tuple.
 have Xii (i : 'I_m) : coord X i X`_i = 1%:R.
-  by rewrite coord_free ?eqxx //; exact (basis_free Xb).
+  by rewrite coord_free ?eqxx //; apply (basis_free Xb).
 have Xij (i j : 'I_m) : j != i -> coord X i X`_j = 0%:R.
-  by rewrite coord_free; [move => /negbTE -> | exact (basis_free Xb)].
+  by rewrite coord_free; [move => /negbTE -> | apply (basis_free Xb)].
 have Xdualb : basis_of fullv Xdual.
   suffices Xdualf : free Xdual.
     rewrite /basis_of Xdualf andbC /= -dimv_leqif_eq ?subvf // eq_sym HomVdim.
@@ -326,7 +331,7 @@ Hypothesis Und : ndeg tr U.
 Hypothesis Xb : basis_of U X.
 
 Lemma dualb_basis : basis_of U dual_basis.
-Proof. have [Yb _] := svalP dual_basis_def Und Xb; exact Yb. Qed.
+Proof. by have [Yb _] := svalP dual_basis_def Und Xb; apply Yb. Qed.
 
 Lemma dualb_orth :
   forall (i : 'I_m), tr X`_i dual_basis`_i = 1 /\
@@ -433,7 +438,7 @@ suffices FisK (F : fieldType) (L0 : fieldExtType F) (A : pred L0) (L : {subfield
   by apply/eqP/XfL0; rewrite -{3}kS => {i}; apply/eq_bigr => i _; rewrite -[RHS]mulr_algl kk'.
 move => Asubr Aint Apid Afrac1 Lnd; pose n := \dim L; have Amulr : mulr_closed A := Asubr.
 have [A0 _] : zmod_closed A := Asubr; have [Asub1 _] := Afrac1.
-have AsubL : {subset A <= L} by move => a /Asub1; exact (subvP (sub1v L) a).
+have AsubL : {subset A <= L} by move => a /Asub1; apply (subvP (sub1v L) a).
 have [b1 [b1B b1H]] : exists (b1 : n.-tuple L0), [/\ basis_of L b1 &
   forall i : 'I_n, integral A b1`_i].
   pose b0 := vbasis L; have [f /all_and3-[fH0 fHa fHi]] := frac_field_alg_int Asubr Afrac1.
diff --git a/mathcomp/attic/all.v b/mathcomp/attic/all.v
deleted file mode 100644
index 41badbb..0000000
--- a/mathcomp/attic/all.v
+++ /dev/null
@@ -1,9 +0,0 @@
-Require Export algnum_basic.
-Require Export amodule.
-Require Export fib.
-Require Export forms.
-Require Export galgebra.
-Require Export multinom.
-Require Export mxtens.
-Require Export quote.
-Require Export tutorial.
diff --git a/mathcomp/attic/amodule.v b/mathcomp/attic/amodule.v
index f23ed60..e9d799e 100644
--- a/mathcomp/attic/amodule.v
+++ b/mathcomp/attic/amodule.v
@@ -1,6 +1,10 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
-Require Import ssreflect ssrbool ssrfun eqtype fintype finfun finset ssralg.
+Require Import mathcomp.ssreflect.ssreflect.
+From mathcomp
+Require Import ssrbool ssrfun eqtype fintype finfun finset ssralg.
+From mathcomp
 Require Import bigop seq tuple choice ssrnat prime ssralg fingroup pgroup.
+From mathcomp
 Require Import zmodp matrix vector falgebra galgebra.
 
 (*****************************************************************************)
@@ -103,7 +107,7 @@ Implicit Types v w: M.
 Implicit Types c: F.
 
 Lemma rmulD x: {morph (rmul^~ x): v1 v2 / v1 + v2}.
-Proof. move=> *; exact: linearD. Qed.
+Proof. by move=> *; apply: linearD. Qed.
 
 Lemma rmul_linear_proof : forall  v, linear (rmul v).
 Proof. by rewrite /rmul /rmorph; case: M => s [] b []. Qed.
@@ -113,10 +117,10 @@ Lemma rmulA v x y: v :* (x * y) = (v :* x) :* y.
 Proof. exact: AModuleType.action_morph. Qed.
 
 Lemma rmulZ : forall c v x, (c *: v) :* x = c *: (v :* x).
-Proof. move=> c v x; exact: linearZZ. Qed.
+Proof. by move=> c v x; apply: linearZZ. Qed.
 
 Lemma rmul0 : left_zero 0 rmul.
-Proof. move=> x; exact: linear0. Qed.
+Proof. by move=> x; apply: linear0. Qed.
 
 Lemma rmul1 : forall v , v :* 1 = v.
 Proof. by rewrite /rmul /rmorph; case: M => s [] b []. Qed.
@@ -154,7 +158,7 @@ Lemma eprodvP : forall vs1 ws vs2,
 Proof.
 move=> vs1 ws vs2; apply: (iffP idP).
   move=> Hs a b Ha Hb.
-  by apply: subv_trans Hs; exact: memv_eprod.
+  by apply: subv_trans Hs; apply: memv_eprod.
 move=> Ha; apply/subvP=> v.
 move/coord_span->; apply: memv_suml=> i _ /=.
 apply: memvZ.
@@ -210,8 +214,8 @@ move=> vs1 vs2 ws; apply subv_anti; apply/andP; split.
   by rewrite rmulD; apply: memv_add; apply: memv_eprod.
 apply/subvP=> v;  case/memv_addP=> v1 Hv1 [v2 Hv2 ->].
 apply: memvD.
-  move: v1 Hv1; apply/subvP; apply: eprodvSl; exact: addvSl.
-move: v2 Hv2; apply/subvP; apply: eprodvSl; exact: addvSr.
+  by move: v1 Hv1; apply/subvP; apply: eprodvSl; apply: addvSl.
+by move: v2 Hv2; apply/subvP; apply: eprodvSl; apply: addvSr.
 Qed.
 
 Lemma eprodv_sumr vs ws1 ws2 : (vs :* (ws1 + ws2) = vs :* ws1 + vs :* ws2)%VS.
@@ -221,8 +225,8 @@ apply subv_anti; apply/andP; split.
   by rewrite linearD; apply: memv_add; apply: memv_eprod.
 apply/subvP=> v;  case/memv_addP=> v1 Hv1 [v2 Hv2 ->].
 apply: memvD.
-  move: v1 Hv1; apply/subvP; apply: eprodvSr; exact: addvSl.
-move: v2 Hv2; apply/subvP; apply: eprodvSr; exact: addvSr.
+  by move: v1 Hv1; apply/subvP; apply: eprodvSr; apply: addvSl.
+by move: v2 Hv2; apply/subvP; apply: eprodvSr; apply: addvSr.
 Qed.
 
 Definition modv (vs: {vspace M}) (al: {aspace A}) :=
@@ -235,7 +239,7 @@ Lemma modv1 : forall vs, modv vs (aspace1 A).
 Proof. by move=> vs; rewrite /modv eprodv1 subvv. Qed.
 
 Lemma modfv : forall al, modv fullv al.
-Proof. by move=> al; exact: subvf. Qed.
+Proof. by move=> al; apply: subvf. Qed.
 
 Lemma memv_mod_mul : forall ms al m a, 
   modv ms al -> m \in ms -> a \in al -> m :* a \in ms.
@@ -273,7 +277,7 @@ Definition completely_reducible ms al :=
 Lemma completely_reducible0 : forall al, completely_reducible 0 al.
 Proof.
 move=> al ms1 Hms1; rewrite subv0; move/eqP->.
-by exists 0%VS; split; [exact: mod0v | exact: cap0v | exact: add0v].
+by exists 0%VS; split; [apply: mod0v | apply: cap0v | apply: add0v].
 Qed.
 
 End AModuleDef.
@@ -394,22 +398,22 @@ have If: limg f = ms1.
     by apply/subvP=> v Hv; rewrite -(Himf _ Hv) memv_img // memvf.
   apply/subvP=> i; case/memv_imgP=> x _ ->.
   rewrite !lfunE memvZ //= sum_lfunE memv_suml=> // j Hj.
-  rewrite lfunE /= lfunE (memv_mod_mul Hms1) //; first by exact: memv_proj.
+  rewrite lfunE /= lfunE (memv_mod_mul Hms1) //; first by apply: memv_proj.
   by rewrite memvE /= /gvspace (bigD1 (j^-1)%g) ?addvSl // groupV.
 exists (ms :&: lker f)%VS; split.
-  - apply: modv_ker=> //; apply/modfP=> *; exact: Cf.
+  - by apply: modv_ker=> //; apply/modfP=> *; apply: Cf.
   apply/eqP; rewrite -subv0; apply/subvP=> v; rewrite memv0.
   rewrite !memv_cap; case/andP=> Hv1; case/andP=> Hv2 Hv3.
   by move: Hv3; rewrite memv_ker  Himf.
-apply: subv_anti; rewrite  subv_add Hsub capvSl.
+apply: subv_anti; rewrite subv_add Hsub capvSl.
 apply/subvP=> v Hv.
 have->: v = f v + (v - f v) by rewrite addrC -addrA addNr addr0.
 apply: memv_add; first by rewrite -If memv_img // memvf.
 rewrite memv_cap; apply/andP; split.
   apply: memvB=> //; apply: subv_trans Hsub.
-  by rewrite -If; apply: memv_img; exact: memvf.
+  by rewrite -If; apply: memv_img; apply: memvf.
 rewrite memv_ker linearB /= (Himf (f v)) ?subrr // /in_mem /= -If.
-by apply: memv_img; exact: memvf. 
+by apply: memv_img; apply: memvf. 
 Qed.
 
 End ModuleRepresentation.
diff --git a/mathcomp/attic/fib.v b/mathcomp/attic/fib.v
index e002a72..b94a06e 100644
--- a/mathcomp/attic/fib.v
+++ b/mathcomp/attic/fib.v
@@ -1,5 +1,8 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
-Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype.
+Require Import mathcomp.ssreflect.ssreflect.
+From mathcomp
+Require Import ssrfun ssrbool eqtype ssrnat seq choice fintype.
+From mathcomp
 Require Import bigop div prime finfun tuple ssralg zmodp matrix binomial.
 
 (*****************************************************************************)
@@ -106,7 +109,7 @@ Proof.
 move=> m n; elim: n=> [|[|n] IH]; first by case: m.
   by case: m{IH}=> [|[]].
 rewrite fibSS leq_eqVlt; case/orP=>[|Hm]; first by move/eqP->.
-by apply: (leq_trans (IH _)) => //; exact: leq_addr.
+by apply: (leq_trans (IH _)) => //; apply: leq_addr.
 Qed.
 
 Lemma fib_eq1 : forall n, (fib n == 1) = ((n == 1) || (n == 2)).
@@ -119,7 +122,7 @@ Lemma fib_eq : forall m n,
   (fib m == fib n) = [|| m == n, (m == 1) && (n == 2) | (m == 2) && (n == 1)].
 Proof.
 move=> m n; wlog: m n/ m <= n=> [HH|].
-  case/orP: (leq_total m n)=> Hm; first by exact: HH.
+  case/orP: (leq_total m n)=> Hm; first by apply: HH.
   by rewrite eq_sym HH // eq_sym ![(_ == 1) && _]andbC [(_ && _) || _] orbC.
 rewrite leq_eqVlt; case/orP=>[|]; first by move/eqP->; rewrite !eqxx.
 case: m=> [|[|m]] Hm.
@@ -170,8 +173,8 @@ Qed.
 Lemma gcdn_fib: forall m n, gcdn (fib m) (fib n) = fib (gcdn m n).
 Proof.
 move=> m n; apply: gcdn_def.
-- by apply: dvdn_fib; exact: dvdn_gcdl.
-- by apply: dvdn_fib; exact: dvdn_gcdr.
+- by apply: dvdn_fib; apply: dvdn_gcdl.
+- by apply: dvdn_fib; apply: dvdn_gcdr.
 move=> d' Hdm Hdn.
 case: m Hdm=> [|m Hdm]; first by rewrite gcdnE eqxx.
 have F: 0 < m.+1 by [].
diff --git a/mathcomp/attic/forms.v b/mathcomp/attic/forms.v
index 1c88af5..5cb7662 100644
--- a/mathcomp/attic/forms.v
+++ b/mathcomp/attic/forms.v
@@ -1,5 +1,8 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
-Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype bigop.
+Require Import mathcomp.ssreflect.ssreflect.
+From mathcomp
+Require Import ssrfun ssrbool eqtype ssrnat seq choice fintype bigop.
+From mathcomp
 Require Import finfun tuple ssralg matrix zmodp vector.
 
 Set Implicit Arguments.
diff --git a/mathcomp/attic/galgebra.v b/mathcomp/attic/galgebra.v
index 411fb6a..3b4004b 100644
--- a/mathcomp/attic/galgebra.v
+++ b/mathcomp/attic/galgebra.v
@@ -1,5 +1,8 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
-Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq choice fintype finfun.
+Require Import mathcomp.ssreflect.ssreflect.
+From mathcomp
+Require Import ssrbool ssrfun eqtype ssrnat seq choice fintype finfun.
+From mathcomp
 Require Import bigop finset ssralg fingroup zmodp matrix vector falgebra.
 
 (*****************************************************************************)
@@ -213,7 +216,7 @@ case/memv_sumP: Hu => u_ Hu ->; rewrite big_distrl /=.
 apply: memv_suml=> i Hi.
 case/memv_sumP: Hv => v_ Hv ->; rewrite big_distrr /=.
 apply: memv_suml=> j Hj.
-rewrite /gvspace (bigD1 (i*j)%g) /=; last by exact: groupM.
+rewrite /gvspace (bigD1 (i*j)%g) /=; last by apply: groupM.
 apply: subv_trans (addvSl _ _).
 case/vlineP: (Hu _ Hi)=> k ->; case/vlineP: (Hv _ Hj)=> l ->.
 apply/vlineP; exists (k * l).
diff --git a/mathcomp/attic/multinom.v b/mathcomp/attic/multinom.v
index b203381..e17d959 100644
--- a/mathcomp/attic/multinom.v
+++ b/mathcomp/attic/multinom.v
@@ -1,5 +1,8 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
-Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype.
+Require Import mathcomp.ssreflect.ssreflect.
+From mathcomp
+Require Import ssrfun ssrbool eqtype ssrnat seq choice fintype.
+From mathcomp
 Require Import tuple finfun bigop ssralg poly generic_quotient bigenough.
 
 (* We build the ring of multinomials with an arbitrary (countable) *)
diff --git a/mathcomp/attic/quote.v b/mathcomp/attic/quote.v
index bde7fac..85c211a 100644
--- a/mathcomp/attic/quote.v
+++ b/mathcomp/attic/quote.v
@@ -1,5 +1,7 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
-Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.
+Require Import mathcomp.ssreflect.ssreflect.
+From mathcomp
+Require Import ssrfun ssrbool eqtype ssrnat seq.
 
 Set Implicit Arguments.
 Unset Strict Implicit.
@@ -99,10 +101,10 @@ Lemma interp_wf_eval : forall y0 e t y,
   interp e t = Some y -> wf t /\ eval y0 e t = y.
 Proof.
 move=> y0 e t; elim/term_ind': t => [i|s a IHa] y /=.
-  by elim: i e => [|i IHi] [|z e] //=; [case | elim: i {IHi} | exact: IHi].
+  by elim: i e => [|i IHi] [|z e] //=; [case | elim: i {IHi} | apply: IHi].
 case: symop => /= n x1.
 elim: n x1 a IHa => [|n IHn] x1 [|f a] //=; first by move=> _  [].
-case: (interp e f) => //= x []; case/(_ x)=> // -> ->; exact: IHn.
+by case: (interp e f) => //= x []; case/(_ x)=> // -> ->; apply: IHn.
 Qed.
 
 Definition var_val := @id T.
@@ -128,7 +130,7 @@ Canonical Structure var_form i x P s := Form (@var_form_subproof i x P s).
 
 Lemma op_form_subproof : forall e t tP (f : form e t tP) x,
   x = @fval e t tP f -> interp e t = Some (op_val x).
-Proof. by move=> e t tP f _ ->; exact: formP. Qed.
+Proof. by move=> e t tP f _ ->; apply: formP. Qed.
 
 Canonical Structure op_form e t tP f x :=
   Form (@op_form_subproof e t tP f x).
@@ -199,7 +201,7 @@ Lemma simp_form : forall e t y ptP,
       (@postProp_statement (close (Env e) /\ simp e t = Some y) ptP),
   fval f = y.
 Proof.
-move=> e t y [tP [_ def_y]] [x /= def_x]; apply: simpP def_y; exact: def_x.
+by move=> e t y [tP [_ def_y]] [x /= def_x]; apply: simpP def_y; apply: def_x.
 Qed.
 
 End GenSimp.
@@ -360,6 +362,6 @@ Time rewrite bsimp.
 Time rewrite !bsimp.
 by [].
 Qed.
-Print try_bsimp.
+
 
 
diff --git a/mathcomp/attic/tutorial.v b/mathcomp/attic/tutorial.v
index 3326c90..52d31cd 100644
--- a/mathcomp/attic/tutorial.v
+++ b/mathcomp/attic/tutorial.v
@@ -1,5 +1,7 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
-Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.
+Require Import mathcomp.ssreflect.ssreflect.
+From mathcomp
+Require Import ssrfun ssrbool eqtype ssrnat seq.
 
 
 Section HilbertSaxiom.
@@ -26,7 +28,7 @@ Qed.
 Check (hAiB hA).
 
 Lemma HilbertS3 : C.
-Proof. by apply: hAiBiC; last exact: hAiB. Qed.
+Proof. by apply: hAiBiC; last apply: hAiB. Qed.
 
 Lemma HilbertS4 : C.
 Proof. exact:  (hAiBiC _ (hAiB _)). Qed.
@@ -226,12 +228,12 @@ move=> m [|d] //=; rewrite -{1}[m]/(0 * d.+1 + m).
 elim: m {-2}m 0 (leqnn m) => [|n IHn] [|m] q //=; rewrite ltnS => le_mn.
 rewrite subn_if_gt; case: ltnP => // le_dm.
 rewrite -{1}(subnKC le_dm) -addSn addnA -mulSnr; apply: IHn.
-apply: leq_trans le_mn; exact: leq_subr.
+by apply: leq_trans le_mn; apply: leq_subr.
 Qed.
 
 Lemma edivn_eq : forall d q r, r < d -> edivn (q * d + r) d = (q, r).
 Proof.
-move=> d q r lt_rd; have d_gt0: 0 < d by exact: leq_trans lt_rd.
+move=> d q r lt_rd; have d_gt0: 0 < d by apply: leq_trans lt_rd.
 case: edivnP lt_rd => q' r'; rewrite d_gt0 /=.
 wlog: q q' r r' / q <= q' by case (ltnP q q'); last symmetry; eauto.
 rewrite leq_eqVlt; case: eqP => [-> _|_] /=; first by move/addnI->.
@@ -254,7 +256,7 @@ move=> m [|d] //=; rewrite -{1}[m]/(0 * d.+1 + m).
 elim: m {-2}m 0 (leqnn m) => [|n IHn] [|m] q //=; rewrite ltnS => le_mn.
 rewrite subn_if_gt; case: ltnP => // le_dm.
 rewrite -{1}(subnKC le_dm) -addSn addnA -mulSnr; apply: IHn.
-apply: leq_trans le_mn; exact: leq_subr.
+by apply: leq_trans le_mn; apply: leq_subr.
 Qed.
 
 Lemma edivnP_right : forall m d, edivn_spec_right m d (edivn m d).
@@ -263,12 +265,12 @@ move=> m [|d] //=; rewrite -{1}[m]/(0 * d.+1 + m).
 elim: m {-2}m 0 (leqnn m) => [|n IHn] [|m] q //=; rewrite ltnS => le_mn.
 rewrite subn_if_gt; case: ltnP => // le_dm.
 rewrite -{1}(subnKC le_dm) -addSn addnA -mulSnr; apply: IHn.
-apply: leq_trans le_mn; exact: leq_subr.
+by apply: leq_trans le_mn; apply: leq_subr.
 Qed.
 
 Lemma edivn_eq_right : forall d q r, r < d -> edivn (q * d + r) d = (q, r).
 Proof.
-move=> d q r lt_rd; have d_gt0: 0 < d by exact: leq_trans lt_rd.
+move=> d q r lt_rd; have d_gt0: 0 < d by apply: leq_trans lt_rd.
 set m := q * d + r; have: m = q * d + r by [].
 set d' := d; have: d' = d by [].
 case: (edivnP_right m d') => {m d'} m d' q' r' -> lt_r'd' d'd q'd'r'.
@@ -282,7 +284,7 @@ Qed.
 
 Lemma edivn_eq_left : forall d q r, r < d -> edivn (q * d + r) d = (q, r).
 Proof.
-move=> d q r lt_rd; have d_gt0: 0 < d by exact: leq_trans lt_rd.
+move=> d q r lt_rd; have d_gt0: 0 < d by apply: leq_trans lt_rd.
 case: (edivnP_left (q * d + r) d) lt_rd; rewrite d_gt0 /=.
 set q':= (edivn (q * d + r) d).1; set r':= (edivn (q * d + r) d).2.
 rewrite (surjective_pairing (edivn (q * d + r) d)) -/q' -/r'.