consistently require-import all_ssreflect instead of pieces of it

src/adt.v

@@ -1,5 +1,4 @@
-From Coq Require Import ssreflect ssrbool ssrfun.
-From mathcomp Require Import eqtype order seq path.
+From mathcomp Require Import all_ssreflect.
 From favssr Require Import bintree bst.
 
 Set Implicit Arguments.

src/avl.v

@@ -1,6 +1,5 @@
 From Equations Require Import Equations.
-From Coq Require Import ssreflect ssrbool ssrfun.
-From mathcomp Require Import eqtype ssrnat ssrint ssralg ssrnum order seq path.
+From mathcomp Require Import all_ssreflect ssrint ssralg ssrnum.
 From favssr Require Import prelude bintree bst adt.
 Set Implicit Arguments.
 Unset Strict Implicit.

src/basics.v

@@ -1,6 +1,5 @@
 From Equations Require Import Equations.
-From Coq Require Import ssreflect ssrbool ssrfun.
-From mathcomp Require Import ssrnat eqtype seq div.
+From mathcomp Require Import all_ssreflect.
 From favssr Require Import prelude.
 Set Implicit Arguments.
 Unset Strict Implicit.

src/beyond.v

@@ -1,6 +1,5 @@
 From Equations Require Import Equations.
-From Coq Require Import ssreflect ssrbool ssrfun.
-From mathcomp Require Import ssrnat eqtype order seq path.
+From mathcomp Require Import all_ssreflect.
 From favssr Require Import prelude bintree bst adt redblack.
 
 Set Implicit Arguments.

src/binom_heap.v

@@ -1,5 +1,4 @@
-From Coq Require Import ssreflect ssrbool ssrfun.
-From mathcomp Require Import ssrnat eqtype order seq path bigop prime binomial.
+From mathcomp Require Import all_ssreflect.
 From favssr Require Import prelude basics priority.
 
 Set Implicit Arguments.
@@ -791,4 +790,4 @@ Fixpoint T_carry (d : nat) (b : seq nat) : nat := 1. (* FIXME *)
 
 Fixpoint T_add (b1 : seq nat) : seq nat -> nat := fun=>1%N. (* FIXME *)
 
-End Exercises.
+End Exercises.

src/bintree.v

@@ -1,6 +1,5 @@
 From Equations Require Import Equations.
-From Coq Require Import ssreflect ssrbool ssrfun.
-From mathcomp Require Import eqtype ssrnat seq prime.
+From mathcomp Require Import all_ssreflect.
 From favssr Require Import prelude.
 Set Implicit Arguments.
 Unset Strict Implicit.
@@ -130,7 +129,7 @@
 
 (* Exercise 4.1 *)
 
 Fixpoint inorder2 (t : tree A) (acc : seq A) : seq A := [::]. (* FIXME *)
 
 Lemma inorder2_correct t xs : inorder2 t xs = inorder t ++ xs.
 Proof.
@@ -267,7 +266,7 @@
 
 (* Exercise 4.2 *)
 
 Fixpoint mcs (t : tree A) : tree A := t. (* FIXME *)
 
 Lemma complete_mcs t : complete (mcs t).
 Proof.
@@ -470,7 +469,7 @@
 
 (* Exercise 4.3 *)
 
 Fixpoint acomplete_rec (t : tree A) : bool :=
   if t is Node l x r then
     false (* FIXME *)
   else true.
@@ -626,7 +625,7 @@
 Definition node_mx (l : tree (P*P)) (a : P) (r : tree (P*P)) : tree (P*P) :=
   @Leaf (P*P).   (* FIXME *)
 
 Fixpoint invar_mx (t : tree (P*P)) : bool :=
   true.  (* FIXME *)
 
 Lemma max_invar t :

src/braun.v

@@ -1,6 +1,5 @@
 From Equations Require Import Equations.
-From Coq Require Import ssreflect ssrbool ssrfun.
-From mathcomp Require Import eqtype ssrnat seq prime bigop ssrAC.
+From mathcomp Require Import all_ssreflect.
 From favssr Require Import prelude bintree.
 
 Set Implicit Arguments.

src/braun_queue.v

@@ -1,6 +1,5 @@
 From Equations Require Import Equations.
-From Coq Require Import ssreflect ssrbool ssrfun.
-From mathcomp Require Import ssrnat eqtype order seq.
+From mathcomp Require Import all_ssreflect.
 From favssr Require Import prelude bintree braun priority.
 
 Set Implicit Arguments.

src/bst.v

@@ -1,6 +1,5 @@
 From Equations Require Import Equations.
-From Coq Require Import ssreflect ssrbool ssrfun.
-From mathcomp Require Import eqtype choice ssrnat seq order path.
+From mathcomp Require Import all_ssreflect.
 From favssr Require Import prelude bintree.
 Set Implicit Arguments.
 Unset Strict Implicit.
@@ -1037,4 +1036,4 @@ Lemma search1_correct t x :
 Proof.
 Admitted.
 
-End IntervalTrees.
+End IntervalTrees.

src/huffman.v

@@ -1,6 +1,5 @@
 From Equations Require Import Equations.
-From Coq Require Import ssreflect ssrbool ssrfun.
-From mathcomp Require Import eqtype ssrnat seq bigop ssrAC.
+From mathcomp Require Import all_ssreflect.
 From favssr Require Import prelude.
 
 Set Implicit Arguments.

src/leftist.v

@@ -1,5 +1,4 @@
-From Coq Require Import ssreflect ssrbool ssrfun.
-From mathcomp Require Import ssrnat eqtype order seq path prime.
+From mathcomp Require Import all_ssreflect.
 From favssr Require Import prelude bintree priority.
 
 Set Implicit Arguments.

src/prelude.v

@@ -1,5 +1,4 @@
-From Coq Require Import ssreflect ssrbool ssrfun.
-From mathcomp Require Import ssrnat eqtype seq order path prime div.
+From mathcomp Require Import all_ssreflect.
 Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
@@ -351,7 +350,7 @@
 case: xs=>//=x xs _; elim/last_ind: xs=>/=.
 - by rewrite lexx inE eq_refl.
 move=>xs y /andP [/andP [IH1 IH2]]; rewrite !inE=>IH3.
 rewrite foldl_rcons le_minl IH1 /= mem_rcons inE eq_minr all_rcons le_minl lexx orbT /=.
 rewrite {1 3 6}/Order.min; case: ifP.
 - by rewrite IH2 /= =>H; case/orP: IH3=>[/eqP->|->]; rewrite ?eqxx ?orbT.
 move/negbT; rewrite -leNgt=>Hy; rewrite Hy /= orbT andbT.
@@ -366,7 +365,7 @@
 Proof.
 move=>Hyx; elim/last_ind: xs=>//=t h IH.
 rewrite all_rcons foldl_rcons; case/andP=>Hy Ha.
 by rewrite le_minr Hy IH.
 Qed.
 
 Lemma all_foldl_eq (x : T) xs :
@@ -426,7 +425,7 @@
 case/andP: (mins_min_in Hy)=>Hay Hiy.
 apply/andP; split.
 - rewrite all_cat; apply/andP; split.
   - by apply/sub_all/Hax=>z Hz; rewrite le_minl Hz.
   by apply/sub_all/Hay=>z Hz; rewrite le_minl Hz orbT.
 rewrite minElt; case: ifP=>_; rewrite mem_cat.
 - by rewrite Hix.

src/priority.v

@@ -1,5 +1,4 @@
-From Coq Require Import ssreflect ssrbool ssrfun.
-From mathcomp Require Import eqtype order seq path.
+From mathcomp Require Import all_ssreflect.
 From favssr Require Import prelude bintree.
 
 Set Implicit Arguments.
@@ -77,7 +76,7 @@
 
 Definition empty_list : seq T := [::].
 
 Fixpoint ins_list (x : T) (xs : seq T) : seq T := xs. (* FIXME *)
 
 Definition del_min_list (xs : seq T) : seq T := xs. (* FIXME *)
 

src/quadtree.v

@@ -1,6 +1,5 @@
 From Equations Require Import Equations.
-From Coq Require Import ssreflect ssrbool ssrfun.
-From mathcomp Require Import eqtype choice ssrnat div bigop ssrAC seq ssralg.
+From mathcomp Require Import all_ssreflect ssralg.
 From favssr Require Import prelude.
 Set Implicit Arguments.
 Unset Strict Implicit.
@@ -318,7 +317,7 @@
 
 (* Exercise 13.1 *)
 
 Fixpoint union (t1 t2 : qtb) : qtb := t1. (* FIXME *)
 
 Lemma height_union t1 t2 : height (union t1 t2) <= maxn (height t1) (height t2).
 Proof.
@@ -337,9 +336,9 @@
 Admitted.
 
 (* this might get in handy *)
 Fixpoint negate (t : qtb) : qtb := t. (* FIXME *)
 
 Fixpoint diff (t1 t2 : qtb) : qtb := t1. (* FIXME *)
 
 Lemma height_diff t1 t2 : height (diff t1 t2) <= maxn (height t1) (height t2).
 Proof.
@@ -654,7 +653,7 @@
 
 Definition shift_mx (f : nat -> nat -> A) (x y i j : nat) : A := f (i+x) (j+y).
 
 Fixpoint qt_of_fun (f : nat -> nat -> A) (n : nat) : qtree A := L (f 0 0). (* FIXME *)
 
 Lemma height_qt_of_fun f n :
   height (qt_of_fun f n) <= n.

src/redblack.v

@@ -1,6 +1,5 @@
 From Equations Require Import Equations.
-From Coq Require Import ssreflect ssrbool ssrfun.
-From mathcomp Require Import eqtype ssrnat prime order seq path.
+From mathcomp Require Import all_ssreflect.
 From favssr Require Import prelude bintree bst adt.
 Set Implicit Arguments.
 Unset Strict Implicit.

src/selection.v

@@ -1,6 +1,5 @@
 From Equations Require Import Equations.
-From Coq Require Import ssreflect ssrbool ssrfun.
-From mathcomp Require Import ssrnat eqtype seq path order bigop div ssrnum ssralg ssrint prime.
+From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint.
 From favssr Require Import prelude sorting.
 Set Implicit Arguments.
 Unset Strict Implicit.

src/sorting.v

@@ -1,6 +1,5 @@
 From Equations Require Import Equations.
-From Coq Require Import ssreflect ssrbool ssrfun.
-From mathcomp Require Import ssrnat eqtype seq path order bigop prime.
+From mathcomp Require Import all_ssreflect.
 From favssr Require Import prelude.
 Set Implicit Arguments.
 Unset Strict Implicit.
@@ -305,7 +304,7 @@
 
 (* Exercise 2.6 *)
 
 Fixpoint halve {A: Type} (xs ys zs : seq A) : seq A * seq A :=
   ([::],[::]). (* FIXME *)
 
 Equations? msort2 xs : seq T by wf (size xs) lt :=

src/trie.v

@@ -1,6 +1,5 @@
 From Equations Require Import Equations.
-From Coq Require Import ssreflect ssrbool ssrfun.
-From mathcomp Require Import eqtype ssrnat seq.
+From mathcomp Require Import all_ssreflect.
 From favssr Require Import prelude bintree adt.
 
 Set Implicit Arguments.

src/twothree.v

@@ -1,6 +1,5 @@
 From Equations Require Import Equations.
-From Coq Require Import ssreflect ssrbool ssrfun.
-From mathcomp Require Import ssrnat eqtype order seq path.
+From mathcomp Require Import all_ssreflect.
 From favssr Require Import prelude bst adt.
 
 Set Implicit Arguments.