Stop depending on all_ssreflect

Author: proux01

theories/polyrcf.v

@@ -1,6 +1,6 @@
 (* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
 (* Distributed under the terms of CeCILL-B.                                  *)
-From mathcomp Require Import all_ssreflect all_algebra polyorder.
+From mathcomp Require Import all_boot order all_algebra polyorder.
 Unset SsrOldRewriteGoalsOrder.  (* remove the line when requiring MathComp >= 2.6 *)
 
 (****************************************************************************)

theories/qe_rcf_th.v

@@ -1,7 +1,7 @@
 (* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
 (* Distributed under the terms of CeCILL-B.                                  *)
 From Corelib Require Import Setoid.
-From mathcomp Require Import all_ssreflect all_algebra.
+From mathcomp Require Import all_boot order all_algebra.
 From mathcomp Require Import polyorder polyrcf mxtens.
 Unset SsrOldRewriteGoalsOrder.  (* remove the line when requiring MathComp >= 2.6 *)
 

theories/realalg.v

@@ -1,7 +1,7 @@
 (* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
 (* Distributed under the terms of CeCILL-B.                                  *)
 From HB Require Import structures.
-From mathcomp Require Import all_ssreflect all_algebra all_field bigenough.
+From mathcomp Require Import all_boot order all_algebra all_field bigenough.
 From mathcomp Require Import polyorder cauchyreals.
 Unset SsrOldRewriteGoalsOrder.  (* remove the line when requiring MathComp >= 2.6 *)