Updating files + reorganizing everything

42 files changed, 181 insertions, 106 deletions

diff --git a/mathcomp/ssrtest/Make b/mathcomp/ssrtest/Make
index adcc2d2..ab4c666 100644
--- a/mathcomp/ssrtest/Make
+++ b/mathcomp/ssrtest/Make
@@ -1,22 +1,20 @@
--R ../theories Ssreflect
--I ../src/
 absevarprop.v
-binders.v
 binders_of.v
+binders.v
 caseview.v
 congr.v
 deferclear.v
 dependent_type_err.v
-elim.v
 elim2.v
 elim_pattern.v
+elim.v
 first_n.v
-gen_pattern.v
 gen_have.v
+gen_pattern.v
 havesuff.v
-have_view_idiom.v
 have_TC.v
 have_transp.v
+have_view_idiom.v
 if_isnt.v
 indetLHS.v
 intro_beta.v
@@ -33,12 +31,14 @@ set_lamda.v
 set_pattern.v
 ssrsyntax1.v
 ssrsyntax2.v
-testmx.v
 tc.v
+testmx.v
 typeof.v
 unkeyed.v
 view_case.v
 wlogletin.v
-wlong_intro.v
 wlog_suff.v
+wlong_intro.v
 
+-R ../theories Ssreflect
+-I ../src/
diff --git a/mathcomp/ssrtest/absevarprop.v b/mathcomp/ssrtest/absevarprop.v
index 513e53f..4fef29e 100644
--- a/mathcomp/ssrtest/absevarprop.v
+++ b/mathcomp/ssrtest/absevarprop.v
@@ -1,5 +1,8 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
-Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq.
+Require Import mathcomp.ssreflect.ssreflect.
+From mathcomp
+Require Import ssrbool ssrfun eqtype ssrnat seq.
+From mathcomp
 Require Import fintype.
 
 Lemma test15: forall (y : nat) (x : 'I_2), y < 1 -> val x = y -> Some x = insub y.
diff --git a/mathcomp/ssrtest/binders.v b/mathcomp/ssrtest/binders.v
index 6a63167..11a8d26 100644
--- a/mathcomp/ssrtest/binders.v
+++ b/mathcomp/ssrtest/binders.v
@@ -1,5 +1,7 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
-Require Import ssreflect ssrbool eqtype ssrnat.
+Require Import mathcomp.ssreflect.ssreflect.
+From mathcomp
+Require Import ssrbool eqtype ssrnat.
 
 Lemma test (x : bool) : True.
 have H1 x := x.
diff --git a/mathcomp/ssrtest/binders_of.v b/mathcomp/ssrtest/binders_of.v
index 70a822e..e8366f6 100644
--- a/mathcomp/ssrtest/binders_of.v
+++ b/mathcomp/ssrtest/binders_of.v
@@ -1,5 +1,7 @@
 
-Require Import ssreflect seq.
+Require Import mathcomp.ssreflect.ssreflect.
+From mathcomp
+Require Import seq.
 
 Lemma test1 : True.
 have f of seq nat & nat : nat.
@@ -7,6 +9,4 @@ have f of seq nat & nat : nat.
 have g of nat := 3.
 have h of nat : nat := 3.
 have _ : f [::] 3 = g 3 + h 4.
-  by admit.
-by admit.
-Qed.
\ No newline at end of file
+Admitted.
diff --git a/mathcomp/ssrtest/caseview.v b/mathcomp/ssrtest/caseview.v
index 108cf46..7b0d4ab 100644
--- a/mathcomp/ssrtest/caseview.v
+++ b/mathcomp/ssrtest/caseview.v
@@ -1,4 +1,5 @@
-Require Import ssreflect.
+Require Import mathcomp.ssreflect.ssreflect.
+
 
 Lemma test (A B : Prop) : A /\ B -> True.
 Proof. by case=> _ /id _. Qed.
\ No newline at end of file
diff --git a/mathcomp/ssrtest/congr.v b/mathcomp/ssrtest/congr.v
index edd52fe..0314772 100644
--- a/mathcomp/ssrtest/congr.v
+++ b/mathcomp/ssrtest/congr.v
@@ -1,5 +1,7 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
-Require Import ssreflect ssrbool eqtype ssrnat.
+Require Import mathcomp.ssreflect.ssreflect.
+From mathcomp
+Require Import ssrbool eqtype ssrnat.
 
 Lemma test1 : forall a b : nat, a == b -> a == 0 -> b == 0.
 Proof. move=> a b Eab Eac; congr (_ == 0) : Eac; exact: eqP Eab. Qed.
diff --git a/mathcomp/ssrtest/deferclear.v b/mathcomp/ssrtest/deferclear.v
index a13a20e..ed57fca 100644
--- a/mathcomp/ssrtest/deferclear.v
+++ b/mathcomp/ssrtest/deferclear.v
@@ -1,5 +1,7 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
-Require Import ssreflect.
+Require Import mathcomp.ssreflect.ssreflect.
+
+From mathcomp
 Require Import ssrbool eqtype fintype ssrnat.
 
 Variable T : Type.
diff --git a/mathcomp/ssrtest/dependent_type_err.v b/mathcomp/ssrtest/dependent_type_err.v
index cd9570b..b2835c7 100644
--- a/mathcomp/ssrtest/dependent_type_err.v
+++ b/mathcomp/ssrtest/dependent_type_err.v
@@ -1,4 +1,6 @@
-Require Import ssreflect ssrfun ssrbool eqtype ssrnat.
+Require Import mathcomp.ssreflect.ssreflect.
+From mathcomp
+Require Import ssrfun ssrbool eqtype ssrnat.
 
 Lemma ltn_leq_trans : forall n m p : nat, m < n -> n <= p -> m < p.
 move=> n m p Hmn Hnp; rewrite -ltnS.
diff --git a/mathcomp/ssrtest/elim.v b/mathcomp/ssrtest/elim.v
index 5ab8f41..1adbb5e 100644
--- a/mathcomp/ssrtest/elim.v
+++ b/mathcomp/ssrtest/elim.v
@@ -1,5 +1,8 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
-Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq.
+Require Import mathcomp.ssreflect.ssreflect.
+From mathcomp
+Require Import ssrbool ssrfun eqtype ssrnat seq.
+Axiom daemon : False. Ltac myadmit := case: daemon.
 
 (* Ltac debugging feature: recursive elim + eq generation *)
 Lemma testL1 : forall A (s : seq A), s = s.
@@ -154,18 +157,19 @@ Proof.
 move=> cf0 cf1 t; split => [] Ecf.
   elim: Ecf.
     match goal with |- forall cf2 cf3 : T, tr cf2 = cf3 -> 
-      execr cf2 cf3 [::] => admit | _ => fail end.
+      execr cf2 cf3 [::] => myadmit | _ => fail end.
   match goal with |- forall (cf2 cf3 cf4 : T) (t0 : seq T),
    tr cf2 = cf4 -> exec cf4 cf3 t0 -> execr cf4 cf3 t0 -> 
-   execr cf2 cf3 (cf4 :: t0) => admit | _ => fail end.
+   execr cf2 cf3 (cf4 :: t0) => myadmit | _ => fail end.
 elim: Ecf.
   match goal with |- forall cf2 : T, 
-    tr cf0 = cf2 -> exec cf0 cf2 [::] => admit | _ => fail end.
+    tr cf0 = cf2 -> exec cf0 cf2 [::] => myadmit | _ => fail end.
 match goal with |- forall (cf2 cf3 : T) (t0 : seq T),
  execr cf0 cf3 t0 -> exec cf0 cf3 t0 -> tr cf3 = cf2 -> 
- exec cf0 cf2 (t0 ++ [:: cf3]) => admit | _ => fail end.
+ exec cf0 cf2 (t0 ++ [:: cf3]) => myadmit | _ => fail end.
 Qed.
 
+From mathcomp
 Require Import seq div prime bigop.
 
 Lemma mem_primes : forall p n,
diff --git a/mathcomp/ssrtest/elim2.v b/mathcomp/ssrtest/elim2.v
index 344ee52..b3e764e 100644
--- a/mathcomp/ssrtest/elim2.v
+++ b/mathcomp/ssrtest/elim2.v
@@ -1,4 +1,7 @@
-Require Import ssreflect eqtype ssrbool ssrnat seq div fintype finfun path bigop.
+Require Import mathcomp.ssreflect.ssreflect.
+From mathcomp
+Require Import eqtype ssrbool ssrnat seq div fintype finfun path bigop.
+Axiom daemon : False. Ltac myadmit := case: daemon.
 
 Lemma big_load R (K K' : R -> Type) idx op I r (P : pred I) F :
   let s := \big[op/idx]_(i <- r | P i) F i in
@@ -13,9 +16,9 @@ Variables (idx : R) (op op' : R -> R -> R).
 
 Hypothesis Kid : K idx.
 
-Ltac ASSERT1 := match goal with |- (K idx) => admit end.
+Ltac ASSERT1 := match goal with |- (K idx) => myadmit end.
 Ltac ASSERT2 K := match goal with |- (forall x1 : R, R -> 
-    forall y1 : R, R -> K x1 -> K y1 -> K (op x1 y1)) => admit end.
+    forall y1 : R, R -> K x1 -> K y1 -> K (op x1 y1)) => myadmit end.
 
 
 Lemma big_rec I r (P : pred I) F
@@ -23,13 +26,13 @@ Lemma big_rec I r (P : pred I) F
   K (\big[op/idx]_(i <- r | P i) F i).
 Proof.
 elim/big_ind2: {-}_.
-  ASSERT1. ASSERT2 K. match goal with |- (forall i : I, is_true (P i) -> K (F i)) => admit end. Undo 4.
+  ASSERT1. ASSERT2 K. match goal with |- (forall i : I, is_true (P i) -> K (F i)) => myadmit end. Undo 4.
 elim/big_ind2: _ / {-}_.
-  ASSERT1. ASSERT2 K. match goal with |- (forall i : I, is_true (P i) -> K (F i)) => admit end. Undo 4.
+  ASSERT1. ASSERT2 K. match goal with |- (forall i : I, is_true (P i) -> K (F i)) => myadmit end. Undo 4.
 
 elim/big_rec2: (\big[op/idx]_(i <- r | P i) op idx (F i))
   / (\big[op/idx]_(i <- r | P i) F i).
-  ASSERT1. match goal with |- (forall i : I, R -> forall y2 : R, is_true (P i) -> K y2 -> K (op (F i) y2)) => admit end. Undo 3.
+  ASSERT1. match goal with |- (forall i : I, R -> forall y2 : R, is_true (P i) -> K y2 -> K (op (F i) y2)) => myadmit end. Undo 3.
 
 elim/(big_load (phantom R)): _.
   Undo.
diff --git a/mathcomp/ssrtest/elim_pattern.v b/mathcomp/ssrtest/elim_pattern.v
index 51ab216..78abb5e 100644
--- a/mathcomp/ssrtest/elim_pattern.v
+++ b/mathcomp/ssrtest/elim_pattern.v
@@ -1,14 +1,17 @@
-Require Import ssreflect ssrbool eqtype ssrnat.
+Require Import mathcomp.ssreflect.ssreflect.
+From mathcomp
+Require Import ssrbool eqtype ssrnat.
+Axiom daemon : False. Ltac myadmit := case: daemon.
 
 Lemma test x : (x == x) = (x + x.+1 == 2 * x + 1).
 case: (X in _ = X) / eqP => _.
-match goal with |- (x == x) = true => admit end.
-match goal with |- (x == x) = false => admit end.
+match goal with |- (x == x) = true => myadmit end.
+match goal with |- (x == x) = false => myadmit end.
 Qed.
 
 Lemma test1 x : (x == x) = (x + x.+1 == 2 * x + 1).
 elim: (x in RHS).
-match goal with |- (x == x) = _ => admit end.
-match goal with |- forall n, (x == x) = _ -> (x == x) = _ => admit end.
+match goal with |- (x == x) = _ => myadmit end.
+match goal with |- forall n, (x == x) = _ -> (x == x) = _ => myadmit end.
 Qed.
 
diff --git a/mathcomp/ssrtest/first_n.v b/mathcomp/ssrtest/first_n.v
index 175684a..e6af0b6 100644
--- a/mathcomp/ssrtest/first_n.v
+++ b/mathcomp/ssrtest/first_n.v
@@ -1,5 +1,7 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
-Require Import ssreflect ssrbool.
+Require Import mathcomp.ssreflect.ssreflect.
+From mathcomp
+Require Import ssrbool.
 
 Lemma test : False -> (bool -> False -> True -> True) -> True.
 move=> F; let w := 2 in apply; last w first.
diff --git a/mathcomp/ssrtest/gen_have.v b/mathcomp/ssrtest/gen_have.v
index 757dba5..59f19d6 100644
--- a/mathcomp/ssrtest/gen_have.v
+++ b/mathcomp/ssrtest/gen_have.v
@@ -1,11 +1,14 @@
-Require Import ssreflect ssrfun ssrbool eqtype ssrnat.
+Require Import mathcomp.ssreflect.ssreflect.
+From mathcomp
+Require Import ssrfun ssrbool eqtype ssrnat.
+Axiom daemon : False. Ltac myadmit := case: daemon.
 
 Axiom P : nat -> Prop.
 Lemma clear_test (b1 b2 : bool) : b2 = b2.
 Proof.
-(* wlog gH : (b3 := b2) / b2 = b3. admit. *)
+(* wlog gH : (b3 := b2) / b2 = b3. myadmit. *)
 gen have {b1} H, gH : (b3 := b2) (w := erefl 3) / b2 = b3.
-  admit.
+  myadmit.
 Fail exact (H b1).
 exact (H b2 (erefl _)).
 Qed.
@@ -13,46 +16,46 @@ Qed.
 
 Lemma test1 n (ngt0 : 0 < n) : P n.
 gen have lt2le, /andP[H1 H2] : n ngt0 / (0 <= n) && (n != 0).
-  match goal with |- is_true((0 <= n) && (n != 0)) => admit end.
+  match goal with |- is_true((0 <= n) && (n != 0)) => myadmit end.
 Check (lt2le : forall n : nat, 0 < n -> (0 <= n) && (n != 0)).
 Check (H1 : 0 <= n).
 Check (H2 : n != 0).
-admit.
+myadmit.
 Qed.
 
 Lemma test2 n (ngt0 : 0 < n) : P n.
 gen have _, /andP[H1 H2] : n ngt0 / (0 <= n) && (n != 0).
-  match goal with |- is_true((0 <= n) && (n != 0)) => admit end.
+  match goal with |- is_true((0 <= n) && (n != 0)) => myadmit end.
 lazymatch goal with
  | lt2le : forall n : nat, is_true(0 < n) -> is_true((0 <= n) && (n != 0))
     |- _ => fail "not cleared"
  | _ => idtac end.
 Check (H1 : 0 <= n).
 Check (H2 : n != 0).
-admit.
+myadmit.
 Qed.
 
 Lemma test3 n (ngt0 : 0 < n) : P n.
 gen have H : n ngt0 / (0 <= n) && (n != 0).
-  match goal with |- is_true((0 <= n) && (n != 0)) => admit end.
+  match goal with |- is_true((0 <= n) && (n != 0)) => myadmit end.
 Check (H : forall n : nat, 0 < n -> (0 <= n) && (n != 0)).
-admit.
+myadmit.
 Qed.
 
 Lemma test4 n (ngt0 : 0 < n) : P n.
 gen have : n ngt0 / (0 <= n) && (n != 0).
-  match goal with |- is_true((0 <= n) && (n != 0)) => admit end.
+  match goal with |- is_true((0 <= n) && (n != 0)) => myadmit end.
 move=> H.
 Check(H : forall n : nat, 0 < n -> (0 <= n) && (n != 0)).
-admit.
+myadmit.
 Qed.
 
 Lemma test4bis n (ngt0 : 0 < n) : P n.
 wlog suff : n ngt0 / (0 <= n) && (n != 0); last first.
-  match goal with |- is_true((0 <= n) && (n != 0)) => admit end.
+  match goal with |- is_true((0 <= n) && (n != 0)) => myadmit end.
 move=> H.
 Check(H : forall n : nat, 0 < n -> (0 <= n) && (n != 0)).
-admit.
+myadmit.
 Qed.
 
 Lemma test5 n (ngt0 : 0 < n) : P n.
@@ -60,7 +63,7 @@ Fail gen have : / (0 <= n) && (n != 0).
 Abort.
 
 Lemma test6 n (ngt0 : 0 < n) : P n.
-gen have : n ngt0 / (0 <= n) && (n != 0) by admit.
+gen have : n ngt0 / (0 <= n) && (n != 0) by myadmit.
 Abort.
 
 Lemma test7 n (ngt0 : 0 < n) : P n.
@@ -70,17 +73,17 @@ Abort.
 Lemma test3wlog2 n (ngt0 : 0 < n) : P n.
 gen have H : (m := n) ngt0 / (0 <= m) && (m != 0).
   match goal with
-    ngt0 : is_true(0 < m) |- is_true((0 <= m) && (m != 0)) => admit end.
+    ngt0 : is_true(0 < m) |- is_true((0 <= m) && (m != 0)) => myadmit end.
 Check (H : forall n : nat, 0 < n -> (0 <= n) && (n != 0)).
-admit.
+myadmit.
 Qed.
 
 Lemma test3wlog3 n (ngt0 : 0 < n) : P n.
 gen have H : {n} (m := n) (n := 0) ngt0 / (0 <= m) && (m != n).
   match goal with
-    ngt0 : is_true(n < m) |- is_true((0 <= m) && (m != n)) => admit end.
+    ngt0 : is_true(n < m) |- is_true((0 <= m) && (m != n)) => myadmit end.
 Check (H : forall m n : nat, n < m -> (0 <= m) && (m != n)).
-admit.
+myadmit.
 Qed.
 
 Lemma testw1 n (ngt0 : 0 < n) : n <= 0.
@@ -88,13 +91,13 @@ wlog H : (z := 0) (m := n) ngt0 / m != 0.
   match goal with
     |- (forall z m,
           is_true(z < m) -> is_true(m != 0) -> is_true(m <= z)) ->
-       is_true(n <= 0) => admit end.
+       is_true(n <= 0) => myadmit end.
 Check(n : nat).
 Check(m : nat).
 Check(z : nat).
 Check(ngt0 : z < m).
 Check(H : m != 0).
-admit.
+myadmit.
 Qed.
 
 Lemma testw2 n (ngt0 : 0 < n) : n <= 0.
@@ -115,9 +118,9 @@ wlog H : {n} (m := n) (z := (X in _ <= X)) ngt0 / m != z.
     |- (forall m z : nat,
           is_true(0 < z) -> is_true(m != z) -> is_true(m <= 0)) -> 
             is_true(n <= 0)   => idtac end.
-  admit.
+  myadmit.
 Fail Check n.
-admit.
+myadmit.
 Qed.
 
 Section Test.
@@ -126,8 +129,8 @@ Definition addx y := y + x.
 
 Lemma testw3 (m n : nat) (ngt0 : 0 < n) : n <= addx x.
 wlog H : (n0 := n) (y := x) (@twoy := (id _ as X in _ <= X)) / twoy = 2 * y.
-  admit.
-admit.
+  myadmit.
+myadmit.
 Qed.
 
 
@@ -140,15 +143,15 @@ wlog H : (y := x) (@twoy := (X in _ <= X)) / twoy = 2 * y.
     |- (forall y : nat,
          let twoy := y + y in
          twoy = 2 * y -> is_true(n + y <= twoy)) ->
-       is_true(n + x <= twox) => admit end.
+       is_true(n + x <= twox) => myadmit end.
 Restart.
 wlog H : (y := x) (@twoy := (id _ as X in _ <= X)) / twoy = 2 * y.
   match goal with
     |- (forall y : nat,
          let twoy := twox in
          twoy = 2 * y -> is_true(n + y <= twoy)) ->
-       is_true(n + x <= twox) => admit end.
-admit.
+       is_true(n + x <= twox) => myadmit end.
+myadmit.
 Qed.
 
 End Test.
@@ -156,5 +159,5 @@ End Test.
 Lemma test_in n k (def_k : k = 0) (ngtk : k < n) : P n.
 rewrite -(add0n n) in {def_k k ngtk} (m := k) (def_m := def_k) (ngtm := ngtk).
 rewrite def_m add0n in {ngtm} (e := erefl 0 ) (ngt0 := ngtm) => {def_m}.
-admit.
+myadmit.
 Qed.
diff --git a/mathcomp/ssrtest/gen_pattern.v b/mathcomp/ssrtest/gen_pattern.v
index de57e8d..e5af827 100644
--- a/mathcomp/ssrtest/gen_pattern.v
+++ b/mathcomp/ssrtest/gen_pattern.v
@@ -1,4 +1,6 @@
-Require Import ssreflect ssrbool ssrnat.
+Require Import mathcomp.ssreflect.ssreflect.
+From mathcomp
+Require Import ssrbool ssrnat.
 
 Notation "( a 'in' c )" := (a + c) (only parsing) : myscope.
 Delimit Scope myscope with myscope.
diff --git a/mathcomp/ssrtest/have_TC.v b/mathcomp/ssrtest/have_TC.v
index 3204c42..de28520 100644
--- a/mathcomp/ssrtest/have_TC.v
+++ b/mathcomp/ssrtest/have_TC.v
@@ -1,4 +1,6 @@
-Require Import ssreflect.
+Require Import mathcomp.ssreflect.ssreflect.
+
+Axiom daemon : False. Ltac myadmit := case: daemon.
 
 Class foo (T : Type) := { n : nat }.
 Instance five : foo nat := {| n := 5 |}.
@@ -14,7 +16,7 @@ have titi : bar _ 5.
   reflexivity.
 have titi2 : bar _ 5 := .
   Fail reflexivity.
-  by admit.
+  by myadmit.
 have totoc (H : bar _ 5) : 3 = 3 := eq_refl.
 move/totoc: nat => _.
 exact I.
@@ -26,10 +28,10 @@ Lemma a' : True.
 set toto := bar _ 8.
 have titi : bar _ 5.
   Fail reflexivity.
-  by admit.
+  by myadmit.
 have titi2 : bar _ 5 := .
   Fail reflexivity.
-  by admit.
+  by myadmit.
 have totoc (H : bar _ 5) : 3 = 3 := eq_refl.
 move/totoc: nat => _.
 exact I.
diff --git a/mathcomp/ssrtest/have_transp.v b/mathcomp/ssrtest/have_transp.v
index f1e3203..3eba582 100644
--- a/mathcomp/ssrtest/have_transp.v
+++ b/mathcomp/ssrtest/have_transp.v
@@ -1,4 +1,6 @@
-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.
 
 
 Lemma test1 n : n >= 0.
diff --git a/mathcomp/ssrtest/have_view_idiom.v b/mathcomp/ssrtest/have_view_idiom.v
index d42a3ac..6faae97 100644
--- a/mathcomp/ssrtest/have_view_idiom.v
+++ b/mathcomp/ssrtest/have_view_idiom.v
@@ -1,5 +1,7 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
-Require Import ssreflect ssrbool.
+Require Import mathcomp.ssreflect.ssreflect.
+From mathcomp
+Require Import ssrbool.
 
 Lemma test (a b : bool) (pab : a && b) : b.
 have {pab} /= /andP [pa -> //] /= : true && (a && b) := pab.
diff --git a/mathcomp/ssrtest/havesuff.v b/mathcomp/ssrtest/havesuff.v
index c497773..b15728d 100644
--- a/mathcomp/ssrtest/havesuff.v
+++ b/mathcomp/ssrtest/havesuff.v
@@ -1,5 +1,6 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
-Require Import ssreflect.
+Require Import mathcomp.ssreflect.ssreflect.
+
 
 Variables P G : Prop.
 
diff --git a/mathcomp/ssrtest/if_isnt.v b/mathcomp/ssrtest/if_isnt.v
index 619df45..58812d5 100644
--- a/mathcomp/ssrtest/if_isnt.v
+++ b/mathcomp/ssrtest/if_isnt.v
@@ -1,4 +1,5 @@
-Require Import ssreflect.
+Require Import mathcomp.ssreflect.ssreflect.
+
 
 Definition unopt (x : option bool) := 
   if x isn't Some x then false else x.
diff --git a/mathcomp/ssrtest/indetLHS.v b/mathcomp/ssrtest/indetLHS.v
index f9d42ff..3f5e7f0 100644
--- a/mathcomp/ssrtest/indetLHS.v
+++ b/mathcomp/ssrtest/indetLHS.v
@@ -1,4 +1,6 @@
-Require Import ssreflect ssrnat.
+Require Import mathcomp.ssreflect.ssreflect.
+From mathcomp
+Require Import ssrnat.
 Goal 5 = 3.
 Fail (rewrite -(addnK _ 5)).
 Abort.
\ No newline at end of file
diff --git a/mathcomp/ssrtest/intro_beta.v b/mathcomp/ssrtest/intro_beta.v
index 6ede976..7a1b0e7 100644
--- a/mathcomp/ssrtest/intro_beta.v
+++ b/mathcomp/ssrtest/intro_beta.v
@@ -1,4 +1,5 @@
-Require Import ssreflect.
+Require Import mathcomp.ssreflect.ssreflect.
+
 
 Axiom T : Type.
 
@@ -9,5 +10,4 @@ Axiom P : T -> T -> Prop.
 Lemma foo : C (fun x => forall y, let z := x in P y x).
 move=> a b. 
 match goal with |- (let y := _ in _) => idtac end.
-admit.
-Qed.
+Admitted.
diff --git a/mathcomp/ssrtest/intro_noop.v b/mathcomp/ssrtest/intro_noop.v
index 91a87b5..be0bea7 100644
--- a/mathcomp/ssrtest/intro_noop.v
+++ b/mathcomp/ssrtest/intro_noop.v
@@ -1,4 +1,7 @@
-Require Import ssreflect ssrbool.
+Require Import mathcomp.ssreflect.ssreflect.
+From mathcomp
+Require Import ssrbool.
+Axiom daemon : False. Ltac myadmit := case: daemon.
 
 Lemma v : True -> bool -> bool. Proof. by []. Qed.
 
@@ -16,8 +19,8 @@ have - -> : a = (id a) by [].
 have --> : a = (id a) by [].
 have - - _ : a = (id a) by [].
 have -{1}-> : a = (id a) by [].
-  by admit.
+  by myadmit.
 move: a.
 case: b => -[] //.
-by admit.
+by myadmit.
 Qed.
diff --git a/mathcomp/ssrtest/ipatalternation.v b/mathcomp/ssrtest/ipatalternation.v
index 9796648..eb29fd7 100644
--- a/mathcomp/ssrtest/ipatalternation.v
+++ b/mathcomp/ssrtest/ipatalternation.v
@@ -1,5 +1,6 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
-Require Import ssreflect.
+Require Import mathcomp.ssreflect.ssreflect.
+
 
 Lemma test1 : Prop -> Prop -> Prop -> Prop -> Prop -> True = False -> Prop -> True \/ True.
 by move=> A /= /= /= B C {A} {B} ? _ {C} {1}-> *; right.
diff --git a/mathcomp/ssrtest/ltac_have.v b/mathcomp/ssrtest/ltac_have.v
index 3ed274d..c106b42 100644
--- a/mathcomp/ssrtest/ltac_have.v
+++ b/mathcomp/ssrtest/ltac_have.v
@@ -1,4 +1,6 @@
-Require Import ssreflect ssrbool ssrnat.
+Require Import mathcomp.ssreflect.ssreflect.
+From mathcomp
+Require Import ssrbool ssrnat.
 
 Ltac SUFF1 h t := suff h x (p := x < 0) : t.
 Ltac SUFF2 h t := suff h x (p := x < 0) : t by apply h.
diff --git a/mathcomp/ssrtest/ltac_in.v b/mathcomp/ssrtest/ltac_in.v
index c9f15dd..4cc0f9c 100644
--- a/mathcomp/ssrtest/ltac_in.v
+++ b/mathcomp/ssrtest/ltac_in.v
@@ -1,4 +1,6 @@
-Require Import ssreflect ssrbool eqtype ssrnat ssrfun.
+Require Import mathcomp.ssreflect.ssreflect.
+From mathcomp
+Require Import ssrbool eqtype ssrnat ssrfun.
 
 Set Implicit Arguments.
 Unset Strict Implicit.
diff --git a/mathcomp/ssrtest/move_after.v b/mathcomp/ssrtest/move_after.v
index 9289193..d62926d 100644
--- a/mathcomp/ssrtest/move_after.v
+++ b/mathcomp/ssrtest/move_after.v
@@ -1,4 +1,5 @@
-Require Import ssreflect.
+Require Import mathcomp.ssreflect.ssreflect.
+
 
 Goal True -> True -> True.
 move=> H1 H2.
diff --git a/mathcomp/ssrtest/multiview.v b/mathcomp/ssrtest/multiview.v
index 53b3b4e..6a4f35b 100644
--- a/mathcomp/ssrtest/multiview.v
+++ b/mathcomp/ssrtest/multiview.v
@@ -1,5 +1,7 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
-Require Import ssreflect ssrbool ssrnat.
+Require Import mathcomp.ssreflect.ssreflect.
+From mathcomp
+Require Import ssrbool ssrnat.
 
 Goal forall m n p, n <= p -> m <= n -> m <= p.
 by move=> m n p le_n_p /leq_trans; apply.
@@ -45,6 +47,7 @@ Lemma test7:  forall A B, (A -> B) -> A -> B.
 move=> A B A_to_B a; apply A_to_B in a; exact: a.
 Qed.
 
+From mathcomp
 Require Import ssrfun eqtype ssrnat div seq choice fintype finfun finset.
 
 Lemma test8 (T : finType) (A B : {set T}) x (Ax : x \in A) (_ : B = A) : x \in B.
diff --git a/mathcomp/ssrtest/occarrow.v b/mathcomp/ssrtest/occarrow.v
index deaee0c..8efa4bc 100644
--- a/mathcomp/ssrtest/occarrow.v
+++ b/mathcomp/ssrtest/occarrow.v
@@ -1,5 +1,7 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
-Require Import ssreflect eqtype ssrnat.
+Require Import mathcomp.ssreflect.ssreflect.
+From mathcomp
+Require Import eqtype ssrnat.
 
 Lemma test1 : forall n m : nat, n = m -> m * m + n * n = n * n + n * n.
 move=> n m E; have [{2}-> _] : n * n = m * n /\ True by move: E => {1}<-.
diff --git a/mathcomp/ssrtest/patnoX.v b/mathcomp/ssrtest/patnoX.v
index 9cde676..75dce69 100644
--- a/mathcomp/ssrtest/patnoX.v
+++ b/mathcomp/ssrtest/patnoX.v
@@ -1,4 +1,6 @@
-Require Import ssreflect ssrbool.
+Require Import mathcomp.ssreflect.ssreflect.
+From mathcomp
+Require Import ssrbool.
 Goal forall x, x && true = x.
 move=> x.
 Fail (rewrite [X in _ && _]andbT).
diff --git a/mathcomp/ssrtest/rewpatterns.v b/mathcomp/ssrtest/rewpatterns.v
index 88c2a2f..33c1903 100644
--- a/mathcomp/ssrtest/rewpatterns.v
+++ b/mathcomp/ssrtest/rewpatterns.v
@@ -1,6 +1,8 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
 
-Require Import ssreflect ssrbool ssrfun eqtype ssrnat.
+Require Import mathcomp.ssreflect.ssreflect.
+From mathcomp
+Require Import ssrbool ssrfun eqtype ssrnat.
 
 Lemma test1 : forall x y (f : nat -> nat), f (x + y).+1 = f (y + x.+1).
 by move=> x y f; rewrite [_.+1](addnC x.+1).
@@ -89,18 +91,16 @@ rewrite [x.+1 + y as X in f X _]addnC.
 match goal with |- (x + y).+1 + f (y + x.+1) (z + (y + x.+1)) = 0 + (0 + 0) => idtac end.
 Admitted.
 
+From mathcomp
 Require Import fintype ssrnat finset fingroup gproduct.
 
 Goal (forall (gT : finGroupType) (G H: {set gT}) (Z : {group gT}), G = Z).
 move=> gT G H K. suff: G \x H = K. case/dprodP=> {G H} [[G H -> -> defK _ _]].
-admit.
-admit.
-Qed.
+Admitted.
 
 Goal (exists x : 'I_3, x > 0).
 apply: (ex_intro _ (@Ordinal _ 2 _)).
-admit.
-Qed.
+Admitted.
 
 Goal (forall y, 1 < y < 2 -> exists x : 'I_3, x > 0).
 move=> y; case/andP=> y_gt1 y_lt2; apply: (ex_intro _ (@Ordinal _ y _)).
@@ -111,8 +111,7 @@ Qed.
 Goal (forall x y : nat, forall P : nat -> Prop, x = y -> True).
 move=> x y P E.
 have: P x -> P y by suff: x = y by move=> ?; congr (P _).
-by admit.
-Qed.
+Admitted.
 
 Goal forall a : bool, a -> true && a || false && a.
 by move=> a ?; rewrite [true && _]/= [_ && a]/= orbC [_ || _]//=.
diff --git a/mathcomp/ssrtest/set_lamda.v b/mathcomp/ssrtest/set_lamda.v
index 51b8e61..432e5d3 100644
--- a/mathcomp/ssrtest/set_lamda.v
+++ b/mathcomp/ssrtest/set_lamda.v
@@ -1,4 +1,6 @@
-Require Import ssreflect ssrbool eqtype ssrnat ssrfun.
+Require Import mathcomp.ssreflect.ssreflect.
+From mathcomp
+Require Import ssrbool eqtype ssrnat ssrfun.
 
 Set Implicit Arguments.
 Unset Strict Implicit.
diff --git a/mathcomp/ssrtest/set_pattern.v b/mathcomp/ssrtest/set_pattern.v
index 0a98267..50dc262 100644
--- a/mathcomp/ssrtest/set_pattern.v
+++ b/mathcomp/ssrtest/set_pattern.v
@@ -1,4 +1,6 @@
-Require Import ssreflect.
+Require Import mathcomp.ssreflect.ssreflect.
+
+Axiom daemon : False. Ltac myadmit := case: daemon.
 
 Ltac T1 x := match goal with |- _ => set t := (x in X in _ = X) end.
 Ltac T2 x := first [set t := (x in RHS)].
@@ -6,6 +8,7 @@ Ltac T3 x := first [set t := (x in Y in _ = Y)|idtac].
 Ltac T4 x := set t := (x in RHS);idtac.
 Ltac T5 x := match goal with |- _ => set t := (x in RHS) | |- _ => idtac end.
 
+From mathcomp
 Require Import ssrbool ssrnat.
 
 Lemma foo x y : x.+1 = y + x.+1.
@@ -31,7 +34,7 @@ rewrite [RHS]addnC.
   match goal with |- x.+1 = x.+1 + y => rewrite -[RHS]addnC end.
 rewrite -[in RHS](@subnK 1 x.+1) //.
   match goal with |- x.+1 = y + (x.+1 - 1 + 1) => rewrite subnK // end.
-have H : x.+1 = y by admit.
+have H : x.+1 = y by myadmit.
 set t := _.+1 in H |- *.
   match goal with H : t = y |- t = y + t => rewrite /t {t} in H * end.
 set t := (_.+1 in X in _ + X) in H |- *.
diff --git a/mathcomp/ssrtest/ssrsyntax1.v b/mathcomp/ssrtest/ssrsyntax1.v
index 64e78da..3a5a731 100644
--- a/mathcomp/ssrtest/ssrsyntax1.v
+++ b/mathcomp/ssrtest/ssrsyntax1.v
@@ -1,5 +1,5 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
-Require ssreflect.
+Require mathcomp.ssreflect.ssreflect.
 Require Import Arith.
 
 Goal (forall a b, a + b = b + a).
diff --git a/mathcomp/ssrtest/ssrsyntax2.v b/mathcomp/ssrtest/ssrsyntax2.v
index 29985b9..c82458d 100644
--- a/mathcomp/ssrtest/ssrsyntax2.v
+++ b/mathcomp/ssrtest/ssrsyntax2.v
@@ -1,4 +1,5 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
+From mathcomp
 Require Import ssrsyntax1.
 Require Import Arith.
 
diff --git a/mathcomp/ssrtest/tc.v b/mathcomp/ssrtest/tc.v
index b3f7d3f..7235a9b 100644
--- a/mathcomp/ssrtest/tc.v
+++ b/mathcomp/ssrtest/tc.v
@@ -1,4 +1,5 @@
-Require Import ssreflect.
+Require Import mathcomp.ssreflect.ssreflect.
+
 
 Class foo (A : Type) : Type := mkFoo { val : A }.
 Instance foo_pair {A B} {f1 : foo A} {f2 : foo B} : foo (A * B) | 2 :=
diff --git a/mathcomp/ssrtest/testmx.v b/mathcomp/ssrtest/testmx.v
index 931cbad..2704a30 100644
--- a/mathcomp/ssrtest/testmx.v
+++ b/mathcomp/ssrtest/testmx.v
@@ -1,5 +1,8 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
-Require Import ssreflect ssrfun ssrbool eqtype ssrnat.
+Require Import mathcomp.ssreflect.ssreflect.
+From mathcomp
+Require Import ssrfun ssrbool eqtype ssrnat.
+From mathcomp
 Require Import ssralg matrix.
 
 Set Implicit Arguments.
diff --git a/mathcomp/ssrtest/typeof.v b/mathcomp/ssrtest/typeof.v
index 8ad81a3..1e1ee8f 100644
--- a/mathcomp/ssrtest/typeof.v
+++ b/mathcomp/ssrtest/typeof.v
@@ -1,4 +1,5 @@
-Require Import ssreflect.
+Require Import mathcomp.ssreflect.ssreflect.
+
 Ltac mycut x :=
   let tx := type of x in
   cut tx.
diff --git a/mathcomp/ssrtest/unkeyed.v b/mathcomp/ssrtest/unkeyed.v
index f6b2021..85b224d 100644
--- a/mathcomp/ssrtest/unkeyed.v
+++ b/mathcomp/ssrtest/unkeyed.v
@@ -1,4 +1,6 @@
-Require Import ssreflect ssrfun ssrbool eqtype.
+Require Import mathcomp.ssreflect.ssreflect.
+From mathcomp
+Require Import ssrfun ssrbool eqtype.
 
 Set Implicit Arguments.
 Unset Strict Implicit.
diff --git a/mathcomp/ssrtest/view_case.v b/mathcomp/ssrtest/view_case.v
index f6de3df..577182a 100644
--- a/mathcomp/ssrtest/view_case.v
+++ b/mathcomp/ssrtest/view_case.v
@@ -1,4 +1,6 @@
-Require Import ssreflect ssrbool ssrnat eqtype seq fintype zmodp.
+Require Import mathcomp.ssreflect.ssreflect.
+From mathcomp
+Require Import ssrbool ssrnat eqtype seq fintype zmodp.
 
 Axiom P : forall T, seq T -> Prop.
 
diff --git a/mathcomp/ssrtest/wlog_suff.v b/mathcomp/ssrtest/wlog_suff.v
index 4e1c86d..a48e770 100644
--- a/mathcomp/ssrtest/wlog_suff.v
+++ b/mathcomp/ssrtest/wlog_suff.v
@@ -1,5 +1,7 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
-Require Import ssreflect ssrbool.
+Require Import mathcomp.ssreflect.ssreflect.
+From mathcomp
+Require Import ssrbool.
 
 Lemma test b : b || ~~b.
 wlog _ : b / b = true.
diff --git a/mathcomp/ssrtest/wlogletin.v b/mathcomp/ssrtest/wlogletin.v
index 4d20321..1ab1c7c 100644
--- a/mathcomp/ssrtest/wlogletin.v
+++ b/mathcomp/ssrtest/wlogletin.v
@@ -1,5 +1,7 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
-Require Import ssreflect eqtype ssrbool.
+Require Import mathcomp.ssreflect.ssreflect.
+From mathcomp
+Require Import eqtype ssrbool.
 
 Variable T : Type.
 Variables P : T -> Prop.
diff --git a/mathcomp/ssrtest/wlong_intro.v b/mathcomp/ssrtest/wlong_intro.v
index 97e378a..977b5eb 100644
--- a/mathcomp/ssrtest/wlong_intro.v
+++ b/mathcomp/ssrtest/wlong_intro.v
@@ -1,4 +1,6 @@
-Require Import ssreflect ssrbool ssrnat.
+Require Import mathcomp.ssreflect.ssreflect.
+From mathcomp
+Require Import ssrbool ssrnat.
 
 Goal (forall x y : nat, True).
 move=> x y.