Adapt to https://github.com/math-comp/math-comp/pull/1545

ecc_classic/alternant.v

@@ -11,6 +11,7 @@ Require Import dft poly_decoding grs bch.
 (******************************************************************************)
 
 Set Implicit Arguments.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 

ecc_classic/bch.v

@@ -21,6 +21,7 @@ Reserved Notation "'\BCHomega_(' a , e )" (at level 0).
 Declare Scope bch_scope.
 
 Set Implicit Arguments.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 

ecc_classic/cyclic_code.v

@@ -36,6 +36,7 @@ Reserved Notation "''cgen[' C ]" (at level 0, format "''cgen[' C ]").
 Declare Scope cyclic_code_scope.
 
 Set Implicit Arguments.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 Unset Strict Implicit.
 Import Prenex Implicits.
 

ecc_classic/decoding.v

@@ -30,6 +30,7 @@ Reserved Notation "t .-BDD f" (at level 2, format "t  .-BDD  f").
 Declare Scope ecc_scope.
 
 Set Implicit Arguments.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 Unset Strict Implicit.
 Import Prenex Implicits.
 

ecc_classic/grs.v

@@ -9,6 +9,7 @@ Require Import ssr_ext ssralg_ext linearcode dft poly_decoding.
 (******************************************************************************)
 
 Set Implicit Arguments.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 

ecc_classic/hamming_code.v

@@ -34,6 +34,7 @@ Require Import binary_symmetric_channel.
 (******************************************************************************)
 
 Set Implicit Arguments.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 Unset Strict Implicit.
 Import Prenex Implicits.
 

ecc_classic/linearcode.v

@@ -46,6 +46,7 @@ Require Import ssr_ext ssralg_ext poly_ext f2 hamming decoding channel_code.
 Import GRing.Theory.
 
 Set Implicit Arguments.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 Unset Strict Implicit.
 Import Prenex Implicits.
 

ecc_classic/mceliece.v

@@ -16,6 +16,7 @@ Require Import ssralg_ext hamming linearcode decoding channel_code.
 Import GRing.Theory.
 
 Set Implicit Arguments.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 Unset Strict Implicit.
 Import Prenex Implicits.
 

ecc_classic/poly_decoding.v

@@ -30,6 +30,7 @@ Reserved Notation "t '.-'rV[' R ]_ n" (at level 2).
 Reserved Notation "'\omega_(' f , a , e )" (at level 0).
 
 Set Implicit Arguments.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 

ecc_classic/reed_solomon.v

@@ -23,6 +23,7 @@ Reserved Notation "'\RSomega_(' a , e )" (at level 0).
 Reserved Notation "'\gen_(' a , d )" (at level 0).
 
 Set Implicit Arguments.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 

ecc_classic/repcode.v

@@ -18,6 +18,7 @@ Require Import hamming num_occ ssralg_ext f2 linearcode decoding channel_code.
 (******************************************************************************)
 
 Set Implicit Arguments.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 Unset Strict Implicit.
 Import Prenex Implicits.
 

ecc_modern/checksum.v

@@ -11,6 +11,7 @@ Require Import pproba.
 (******************************************************************************)
 
 Set Implicit Arguments.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 Unset Strict Implicit.
 Import Prenex Implicits.
 

ecc_modern/degree_profile.v

@@ -18,6 +18,7 @@ Require Import ssr_ext ssralg_ext fdist.
 (******************************************************************************)
 
 Set Implicit Arguments.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 

ecc_modern/ldpc.v

@@ -20,6 +20,7 @@ Require Import channel_code summary checksum summary_tanner.
 (******************************************************************************)
 
 Set Implicit Arguments.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 Unset Strict Implicit.
 Import Prenex Implicits.
 

ecc_modern/ldpc_algo.v

@@ -21,6 +21,7 @@ Require Import tanner_partition summary ldpc checksum.
 (******************************************************************************)
 
 Set Implicit Arguments.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 Unset Strict Implicit.
 Import Prenex Implicits.
 

ecc_modern/ldpc_algo_proof.v

@@ -17,6 +17,7 @@ Require Import tanner_partition summary ldpc checksum ldpc_algo.
 (******************************************************************************)
 
 Set Implicit Arguments.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 Unset Strict Implicit.
 Import Prenex Implicits.
 

ecc_modern/ldpc_erasure.v

@@ -17,6 +17,7 @@ Declare Scope letter_scope.
 Declare Scope bec_scope.
 
 Set Implicit Arguments.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 Unset Strict Implicit.
 Import Prenex Implicits.
 

ecc_modern/max_subset.v

@@ -7,6 +7,7 @@ From mathcomp Require Import all_ssreflect.
 (******************************************************************************)
 
 Set Implicit Arguments.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 

ecc_modern/stopping_set.v

@@ -26,6 +26,7 @@ Require Import num_occ hamming ldpc_erasure tanner linearcode.
 (******************************************************************************)
 
 Set Implicit Arguments.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 

ecc_modern/subgraph_partition.v

@@ -9,6 +9,7 @@ Require Import ssr_ext.
 (******************************************************************************)
 
 Set Implicit Arguments.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 Unset Strict Implicit.
 Import Prenex Implicits.
 

ecc_modern/summary.v

@@ -28,6 +28,7 @@ Reserved Notation "\sum_ ( x '=' d [~ s ] '|' P ) F"
 Declare Scope summary_scope.
 
 Set Implicit Arguments.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 Unset Strict Implicit.
 Import Prenex Implicits.
 

ecc_modern/summary_tanner.v

@@ -21,6 +21,7 @@ Require Import checksum.
 *)
 
 Set Implicit Arguments.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 Unset Strict Implicit.
 Import Prenex Implicits.
 

ecc_modern/tanner.v

@@ -18,6 +18,7 @@ Reserved Notation "''V(' x ',' y ')'" (format "''V(' x ','  y ')'").
 Reserved Notation "''F(' x ',' y ')'" (format "''F(' x ','  y ')'").
 
 Set Implicit Arguments.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 Unset Strict Implicit.
 Import Prenex Implicits.
 

ecc_modern/tanner_partition.v

@@ -10,6 +10,7 @@ Require Import ssr_ext subgraph_partition tanner f2.
 (******************************************************************************)
 
 Set Implicit Arguments.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 Unset Strict Implicit.
 Import Prenex Implicits.
 

information_theory/aep.v

@@ -20,6 +20,7 @@ Require Import fdist proba entropy.
 (******************************************************************************)
 
 Set Implicit Arguments.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 Unset Strict Implicit.
 Import Prenex Implicits.
 

information_theory/binary_symmetric_channel.v

@@ -21,6 +21,7 @@ Require Import channel_code pproba.
 (******************************************************************************)
 
 Set Implicit Arguments.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 Unset Strict Implicit.
 Import Prenex Implicits.
 

information_theory/channel.v

@@ -32,6 +32,7 @@ Require Import proba entropy jfdist_cond.
 (******************************************************************************)
 
 Set Implicit Arguments.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 Unset Strict Implicit.
 Import Prenex Implicits.
 

information_theory/channel_code.v

@@ -31,6 +31,7 @@ Reserved Notation "scha( W , C )" (at level 50).
 Declare Scope channel_code_scope.
 
 Set Implicit Arguments.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 Unset Strict Implicit.
 Import Prenex Implicits.
 

information_theory/channel_coding_converse.v

@@ -18,6 +18,7 @@ Require Import error_exponent channel_code channel success_decode_bound.
 (******************************************************************************)
 
 Set Implicit Arguments.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 Unset Strict Implicit.
 Import Prenex Implicits.
 

information_theory/channel_coding_direct.v

@@ -31,6 +31,7 @@ Require Import channel_code.
 (******************************************************************************)
 
 Set Implicit Arguments.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 Unset Strict Implicit.
 Import Prenex Implicits.
 

information_theory/conditional_divergence.v

@@ -16,6 +16,7 @@ Reserved Notation "'D(' V '||' W '|' P ')'"
   (at level 50, V, W, P at next level).
 
 Set Implicit Arguments.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 Unset Strict Implicit.
 Import Prenex Implicits.
 

information_theory/entropy.v

@@ -33,6 +33,7 @@ Require Import fdist jfdist_cond proba binary_entropy_function divergence.
 (******************************************************************************)
 
 Set Implicit Arguments.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 Unset Strict Implicit.
 Import Prenex Implicits.
 

information_theory/entropy_convex.v

@@ -38,6 +38,7 @@ Require Import binary_entropy_function log_sum divergence.
 (******************************************************************************)
 
 Set Implicit Arguments.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 Unset Strict Implicit.
 Import Prenex Implicits.
 

information_theory/erasure_channel.v

@@ -15,6 +15,7 @@ Require Import entropy binary_entropy_function channel hamming channel_code.
 (******************************************************************************)
 
 Set Implicit Arguments.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 Unset Strict Implicit.
 Import Prenex Implicits.
 

information_theory/error_exponent.v

@@ -29,6 +29,7 @@ Require Import variation_dist pinsker.
 (******************************************************************************)
 
 Set Implicit Arguments.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 Unset Strict Implicit.
 Import Prenex Implicits.
 

information_theory/joint_typ_seq.v

@@ -41,6 +41,7 @@ Declare Scope jtyp_seq_scope.
 Reserved Notation "'`JTS'".
 
 Set Implicit Arguments.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 Unset Strict Implicit.
 Import Prenex Implicits.
 

information_theory/jtypes.v

@@ -35,6 +35,7 @@ Reserved Notation "'\nu^{' B '}' '(' P ')'" (at level 0,
 Reserved Notation "'`tO(' V )" (at level 0).
 
 Set Implicit Arguments.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 Unset Strict Implicit.
 Import Prenex Implicits.
 

information_theory/kraft.v

@@ -29,6 +29,7 @@ Require Import ssr_ext.
 (******************************************************************************)
 
 Set Implicit Arguments.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 

information_theory/pproba.v

@@ -30,6 +30,7 @@ Reserved Notation "P ''_' n0 '`^^' W '(' a '|' y ')'" (at level 1,
 Reserved Notation "P .-receivable W" (at level 2, format "P .-receivable  W").
 
 Set Implicit Arguments.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 Unset Strict Implicit.
 Import Prenex Implicits.
 

information_theory/shannon_fano.v

@@ -20,6 +20,7 @@ Require Import ssr_ext bigop_ext realType_ext realType_ln fdist entropy kraft.
 (******************************************************************************)
 
 Set Implicit Arguments.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 

information_theory/source_code.v

@@ -16,6 +16,7 @@ Require Import realType_ln fdist proba.
 (******************************************************************************)
 
 Set Implicit Arguments.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 Unset Strict Implicit.
 Import Prenex Implicits.
 

information_theory/source_coding_fl_converse.v

@@ -18,6 +18,7 @@ Require Import typ_seq source_code.
 (******************************************************************************)
 
 Set Implicit Arguments.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 Unset Strict Implicit.
 Import Prenex Implicits.
 

information_theory/source_coding_fl_direct.v

@@ -17,6 +17,7 @@ Require Import proba entropy aep typ_seq source_code.
 (******************************************************************************)
 
 Set Implicit Arguments.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 Unset Strict Implicit.
 Import Prenex Implicits.
 

information_theory/source_coding_vl_converse.v

@@ -20,6 +20,7 @@ Require Import fdist proba entropy divergence log_sum source_code.
 (******************************************************************************)
 
 Set Implicit Arguments.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 

information_theory/source_coding_vl_direct.v

@@ -22,6 +22,7 @@ Require Import fdist proba entropy aep typ_seq natbin source_code.
 (******************************************************************************)
 
 Set Implicit Arguments.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 

information_theory/string_entropy.v

@@ -20,6 +20,7 @@ Require Import fdist entropy convex jensen num_occ.
 (******************************************************************************)
 
 Set Implicit Arguments.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 Unset Strict Implicit.
 Import Prenex Implicits.
 

information_theory/success_decode_bound.v

@@ -31,6 +31,7 @@ Require Import entropy channel_code channel.
 (******************************************************************************)
 
 Set Implicit Arguments.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 Unset Strict Implicit.
 Import Prenex Implicits.
 

information_theory/typ_seq.v

@@ -31,6 +31,7 @@ Declare Scope typ_seq_scope.
 Reserved Notation "'`TS'".
 
 Set Implicit Arguments.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 Unset Strict Implicit.
 Import Prenex Implicits.
 

information_theory/types.v

@@ -35,6 +35,7 @@ Reserved Notation "P '.-typed_code' c" (at level 50, c at next level).
 Declare Scope types_scope.
 
 Set Implicit Arguments.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 Unset Strict Implicit.
 Import Prenex Implicits.
 

lib/bigop_ext.v

@@ -10,6 +10,7 @@ Require Import ssr_ext ssralg_ext.
 (******************************************************************************)
 
 Set Implicit Arguments.
+Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
 Unset Strict Implicit.
 Import Prenex Implicits.